[isabelle-dev] adhoc overloading

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Jun 10 20:34:41 CEST 2013

>> There is no point to do
>> such low-level optimizations in the syntax layer.  It is for hardcore
>> kernel operations only
> So should I manually check the result for equality, or does the
> framework do this for me?


There are two variants of interfaces adding functions to check phases:
one with explicit hinting by the check function via None/Some, the other
one with check by the framework.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130610/18ed03a2/attachment.sig>

More information about the isabelle-dev mailing list