(Examples also included in attached file char_tuple_issue.sml)
After defining e.g.
[T]
S %def% [X : T]
the type inference issue with characteristic tuples can be seen when the
term
{S; S'}
occurs as a subterm. For example, the following terms fail when they
are being constructed, d
I've noticed that the ProofPower-Z grammar accepts lambda expressions
without a spot, e.g.
(%lambda% x : X)
because it uses the same grammar rules as for mu expressions. Such
expressions always produce the error message
Exception PARSER_ERROR: PARSER_ERROR "invalid PredLambda arguments" r
