[Agda] more unification using more complex with abstractions

Nils Anders Danielsson nad at cse.gu.se
Sat Aug 4 19:21:37 CEST 2018


On 2018-07-31 20:00, rick wrote:
> Can I use the lemma and if so how can I use it to cause Agda to unify
> mu?

{-# BUILTIN EQUALITY _==_ #-}

mu : ∀ {X} (xss : List (List X)) →
      listMap (unit >> mult) xss == xss
mu []           = refl []
mu (xs₁ ,- xs₂) rewrite lem xs₁ | mu xs₂ = refl _

-- 
/NAD


More information about the Agda mailing list