[Agda] A puzzle with "with"

[Nils Anders Danielsson]

On 2009-06-25 17:44, Ana Bove wrote:
> And I must say I do not understand why. I never used inspect before
> but I thought the difference with inspect was that not only gave me
> the result I would get without inspect but also the "evidence" of that
> result.

You get the result and a proof that the result matches the "with
expression". However, if you pattern match on the proof (refl) you lose
the connection with the with expression, and if you don't pattern match
the goal type and context are not updated with the result. One
workaround is to use subst (substitutivity of _≡_) in the right-hand
side, another is to abandon the use of with.

Ulf, would it be hard to implement parsing of "f args | e"? That feature
would make it easier to prove things about functions defined using with
without using with in the proofs.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.