[Agda] Inference for invariant arguments question
Andrea Vezzosi
sanzhiyan at gmail.com
Sun Oct 6 00:34:53 CEST 2013
Hi,
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?
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
-- Andrea
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131006/0845247e/attachment.html
More information about the Agda
mailing list