[Agda] Trouble with the 'with' clause

Balaji Rao balaji at raobalaji.com
Mon Feb 10 13:10:12 CET 2014


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


More information about the Agda mailing list