(%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" raisedbecause there is no support for generating the characteristic tuple of a lambda expression.
Is/was there some intention of allowing lambda expressions without a spot to construct an identity function? I can't see that this is much use because the toolkit function "id" is just as good and in some cases, better, e.g.
(%lambda% x : X | p x) = id {x : X | p x}
(%lambda% x : X) = id X
Attached is a fairly mundane patch that adapts the grammar for lambda
expressions. Then e.g.
(%lambda% x : X) produces a regular syntax error. Phil
patch-2.9.1w2.pbc.110605.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
