>> 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?
See http://isabelle.in.tum.de/repos/isabelle/file/41d7946e2595/src/Pure/Syntax/syntax_phases.ML#l854 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. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
