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

[Andreas Abel]

g : ps ≡ [] → f ps ≡ 1
g p rewrite p = PE.refl


On 05.02.2016 06:24, effectfully wrote:
> Also
>      g : ps ≡ [] → f ps ≡ 1
>      g r with ps | r
>      ... | []    | _ = PE.refl
>      ... | _ ∷ _ | ()

You can do with one clause here if you match on r instead of ps after 
the with.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/