Re: [Agda] "xs ≡ [] → " question

effectfully effectfully at gmail.com
Fri Feb 5 06:24:01 CET 2016 

Also
    g : ps ≡ [] → f ps ≡ 1
    g r with ps | r
    ... | []    | _ = PE.refl
    ... | _ ∷ _ | ()

More information about the Agda mailing list