[isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31

Andrei Popescu uuomul at yahoo.com
Sat May 24 20:25:56 CEST 2014

Makarius wrote: 

>> Can you explain the squiggle =: above?  I did not find it in the manual
>> nor in the sources so far.  It seems to be special to main HOL datatypes.

I had not even noticed that weird-looking combination of symbols.    :-)

Now I see that what it does is indicate for Nil that a discriminator (of type "'a list => bool") 

should not be provided, but instead equality with Nil should be used.  

This option seems to only be available for nullary constructors.  


More information about the isabelle-dev mailing list