[Agda] with x =? x

[Andrea Vezzosi]

You could prove that  "x ≟ x" equals "yes refl" in a separate lemma
(by using "with x ≟ x") and use rewrite with that lemma in foo,
that way you don't have to care about the "no .." case there.

Cheers,
Andrea

On Wed, Dec 31, 2014 at 3:31 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> People,
> I discover that Agda requires even  " with k ≟ k" :
>
>   foo : .. -> ins (k , v) (ins (k , u) ps)  =pn  ins (k , comb k v u) ps
>
>   foo {k} {u} {v} {[]}  with k ≟ k
>   ...                 | yes _  =  =pn-refl          -- instance of  refl
>   ...                 | no k≉k =  ⊥-elim $ k≉k ≈refl
>
> _=pn_ is the pointwise equality for lists of certain pairs, when pairs
> are compared by a certain _=p_.
> ins  inserts a pair into a list "by the key". It compares  k ≟ k',  and
> acts respectively.
> And in  foo,   ins  is applied with   k for k'.
>
> And a mere  " =pn-refl"  is not sufficient!
> I have satisfied `ins' only with `with'.
>
> This looks like a minor feature, but still:
> is there a way to write nicer proofs than by using  "with x ≟ x"
> ?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda