Thanks Guillaume, this point is clear to me now.
Le 21/09/2020 à 14:03, Guillaume Melquiond a écrit :
Le 21/09/2020 à 13:42, Alain Giorgetti a écrit :
What is the purpose of 'meta coercion function', often used in the
standard library?
A coercion is automatically inserted whenever the type ch
Le 21/09/2020 à 13:42, Alain Giorgetti a écrit :
> What is the purpose of 'meta coercion function', often used in the
> standard library?
A coercion is automatically inserted whenever the type checker
encounters an error. For example, if a value of type x is expected, but
a value v of type y is p
Hello,
What is the purpose of 'meta coercion function', often used in the
standard library?
I understand that this statement declares a coercion, but what impact
does it have on proofs, if any?
Best regards,
Alain
___
Why3-club mailing list
Why3-
