[Agda] Rewriting in general

[Nils Anders Danielsson]

On 2016-01-27 20:34, Owen wrote:
> That is, pattern matching on _≡_ introduces new definitional
> equalities that cause the LHS to reduce to the RHS [...]

The LHS and the RHS are /unified/. Example:

Before pattern matching:

   foo : ∀ x xs → 4 ∷ xs ≡ x ∷ [] → x ≡ 4
   foo x xs eq = ?

   eq:   4 ∷ xs ≡ x ∷ []
   Goal: x ≡ 4

After pattern matching:

   foo : ∀ x xs → 4 ∷ xs ≡ x ∷ [] → x ≡ 4
   foo .4 .[] refl = ?

   Goal: 4 ≡ 4

-- 
/NAD