<div dir="ltr">Hi,<div><br></div><div>currently agda won't accept code like this:</div><div><br></div><div><div>test0 : ∀ {F : ℕ -> ℕ} -> (\ x -> suc (F x)) ≡ (\ x -> suc (suc x)) -> ℕ</div><div>test0 {.suc} refl = ?</div>
</div><div><br></div><div>reporting that "F x" is not the same as "suc x".</div><div><br></div><div>Interestingly we can actually derive "F ≡ suc" through "cong (\ f x -> pred (f x)) p", and in general instead of pred we can use a function like strip</div>
<div><br></div><div>strip x (con y) = y</div><div>strip x _ = G x</div><div><br></div><div>to handle equations like (\x -> con (F x)) ≡ (\x -> con (G x)).</div><div><br></div><div>Such equations come up all the time when trying to do induction on representations in the style of "Outrageous but Meaningful Coincidences"[1], so it'd be nice to have native support.</div>
<div><br></div><div>It would actually be great to be able to recognize as empty things like </div><div>(\ (x : A) -> true) ≡ (\ x -> false), but that seems refutable only when you have an element of A.</div><div><br>
</div><div> </div><div>Cheers,</div><div>Andrea</div><div><br></div><div>[1]<a href="http://dl.acm.org/citation.cfm?id=1863497">http://dl.acm.org/citation.cfm?id=1863497</a></div><div><br></div><div><br></div><div><br></div>
<div><br></div><div><br></div><div><br></div></div>