What is =/=> for?

Google Group
1

Say that you have the following form of code:

case+ v of
| pat1 => …
| pat2 => …
| pat3 =/=> myproof

When typechecking the third clause, the typechecker will make sure that
myproof
proves falsehood. During compilation (after typechecking). the third clause
is removed
as it can never be chosen at run-time (because matching v against yields
falsehood).

2

This feature is not common used. I have only used it in proof construction.
For instance, you can find two uses of =/=> in the following code:

The second use is a genuine use of this feature.On Friday, November 22, 2013 4:33:52 PM UTC-5, William Blair wrote:

Could you upload an example of this feature?

On Thursday, November 21, 2013 9:54:51 PM UTC-5, gmhwxi wrote:

Say that you have the following form of code:

case+ v of
| pat1 => …
| pat2 => …
| pat3 =/=> myproof

When typechecking the third clause, the typechecker will make sure that
myproof
proves falsehood. During compilation (after typechecking). the third
clause is removed
as it can never be chosen at run-time (because matching v against yields
falsehood).

3

Could you upload an example of this feature?On Thursday, November 21, 2013 9:54:51 PM UTC-5, gmhwxi wrote:

Say that you have the following form of code:

case+ v of
| pat1 => …
| pat2 => …
| pat3 =/=> myproof

When typechecking the third clause, the typechecker will make sure that
myproof
proves falsehood. During compilation (after typechecking). the third
clause is removed
as it can never be chosen at run-time (because matching v against yields
falsehood).