History log of /seL4-l4v-master/HOL4/src/parse/FCNet.sig
Revision Date Author Comments
# 32e10640 08-Nov-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Give minimal documentation for FCNet module in comment

Also flag a possible bug


# b847c215 01-Aug-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Extract pretty-printing of LET-terms from term_pp.sml

It is now part of user-printer "land" in src/bool/boolpp.sml,
alongside the custom printer for if-then-else (COND).

This refactoring revealed a bug in the way overloaded constants
couldn't be handled by user-printers if they could have extra
arguments hanging off to the right (as in “LET f x y”), *unless* they
were overloaded to "case" (as in COND).

To make sure one's user-printer is going to work, you have to consult
the grammar's overload information to check if your term is one you
want to print according to the grammar_name function. Unfortunately,
looking for particular constants is not guaranteed to work, as the
process of descending terms in the pretty-printer is liable to turn
real constants into special "fake" constants that are actually
variables with special names.

This is progress with Github issue #154, to allow new (Isabelle-style)
syntax for let expressions.