Phil,
On 5 Jun 2011, at 22:53, Phil Clayton wrote:
> 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?
No. Just one of those things.
> 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.
Thanks.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
