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" raised

because 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.


Attachment: patch-2.9.1w2.pbc.110605.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to