[Agda] Trouble with the 'with' clause

[Liam O'Connor]

It’s not a bug. Agda will only accept refl if f a and b normalise to the same result.

What you probably want to do here is use the inspect idiom, which gives you a proof of equality for the pattern matching:

  g : ∀ {a} → a ≡ a 
  g {a} with f a | inspect f a  
  ... | b | [ eq ] = h b eq

On 10 February 2014 at 11:10:33 pm, Balaji Rao (balaji at raobalaji.com) wrote:

Hi,  

I ran into a problem with the ‘with’ clause and here’s a silly demonstration.   

--  
open import Data.Nat  
open import Relation.Binary.PropositionalEquality  

module Test where  
  postulate  
    f : ℕ → ℕ  
    h : ∀ {a} (b : ℕ) → f a ≡ b → a ≡ a  
      
  g : ∀ {a} → a ≡ a  
  g {a} with f a   
  ... | b = h b {!!}   
—  

I end up with a goal to prove f a = b, and refl doesn’t work. Is it a bug ?  

--   
Balaji  
_______________________________________________  
Agda mailing list  
Agda at lists.chalmers.se  
https://lists.chalmers.se/mailman/listinfo/agda  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140211/58c4f789/attachment.html