<html><head><style>body{font-family:Helvetica,Arial;font-size:13px}</style></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">It’s not a bug. Agda will only accept refl if f a and b normalise to the same result.</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">What you probably want to do here is use the inspect idiom, which gives you a proof of equality for the pattern matching:</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><blockquote type="cite" class="clean_bq"></blockquote> g : ∀ {a} → a ≡ a <br><blockquote type="cite" class="clean_bq"></blockquote> g {a} with f a | inspect f a <br> ... | b | [ eq ] = h b eq</div> <br><p style="color:#A0A0A8;">On 10 February 2014 at 11:10:33 pm, Balaji Rao (<a href="mailto://balaji@raobalaji.com">balaji@raobalaji.com</a>) wrote:</p> <blockquote type="cite" class="clean_bq"><span><div><div>Hi,
<br>
<br>I ran into a problem with the ‘with’ clause and here’s a silly demonstration.
<br>
<br>--
<br>open import Data.Nat
<br>open import Relation.Binary.PropositionalEquality
<br>
<br>module Test where
<br> postulate
<br> f : ℕ → ℕ
<br> h : ∀ {a} (b : ℕ) → f a ≡ b → a ≡ a
<br>
<br> g : ∀ {a} → a ≡ a
<br> g {a} with f a
<br> ... | b = h b {!!}
<br>—
<br>
<br>I end up with a goal to prove f a = b, and refl doesn’t work. Is it a bug ?
<br>
<br>--
<br>Balaji
<br>_______________________________________________
<br>Agda mailing list
<br>Agda@lists.chalmers.se
<br>https://lists.chalmers.se/mailman/listinfo/agda
<br></div></div></span></blockquote></body></html>