[Agda] " | condition " in report

[Andreas Abel]

The "| condition" refers to the call to a with-function.

(Continue below.)

On 19.12.13 7:22 PM, Sergei Meshveliani wrote:
...
> lemma : (k v : ℕ) → (ps : List (ℕ × ℕ)) → let keys = getKeys ps
>                                                ps'  = insert k v ps
>                                            in
>                                            k ∈ keys → getKeys ps' ≡ keys
>
> lemma _ _ []               ()
> lemma k _ ((k' , _) ∷ ps)  (here k=k')  with  k ≟ k'
> ...                                     | yes _   =  PE.refl
> ...                                     | no k≉k' =  ⊥-elim (k≉k' k=k')
>
> lemma k v ((k' , v') ∷ ps) (there k∈ks)  with  k ≟ k'
> ... |
>        yes k=k' =  PE.refl
> ... | no k≢k'  =  goal

This proof is completed simply by

... | no k≢k'  =  PE.cong (_∷_ k') (lemma k v ps k∈ks)

Merry Christmas,
Andreas

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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