[Agda] Inference for invariant arguments question
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Oct 22 22:22:48 CEST 2013
Sorry, I somehow overlooked your message...
On 06.10.2013 00:34, Andrea Vezzosi wrote:
> In the following the _ in "yellow" is not resolved while the one in
> "inferred" is.
> Is it because g is not invariant in that argument and so it matters what
> we pass to it?
Exactly, yes!
The _ in inferred is resolved by instance search, since f does not
depend on it. However, g z might depend on z (we do not know since we
do not know how g behaves...).
Cheers,
Andreas
> open import Relation.Binary.PropositionalEquality
>
> data X : Set where
> x : X
>
> f : X -> X -> Set
> f _ x = X
>
> postulate
> stuck : X
> g : ∀ z -> f z stuck
>
> yellow : ∀ z -> f z stuck
> yellow z = g _
> inferred : ∀ z -> f _ ≡ f z
> inferred z = refl
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list