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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to