[Agda] " | condition " in report
mechvel at botik.ru
Sat Dec 28 13:56:14 CET 2013
On Sun, 2013-12-22 at 21:35 +0100, Andreas Abel wrote:
> 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,
Thank you. This was silly of me to overlook such a natural proof.
There remains a question:
why the checker does not accept my awkward proof for goal ?
Is it a bug?
More information about the Agda