# The `@[eqns]` attribute #

This file provides the `eqns` attribute as a way of overriding the default equation lemmas. For example

    def transpose {m n} (A : m → n → ℕ) : n → m → ℕ
      | i, j => A j i

    theorem transpose_apply {m n} (A : m → n → ℕ) (i j) :
        transpose A i j = A j i := rfl

    attribute [eqns transpose_apply] transpose

    theorem transpose_const {m n} (c : ℕ) :
        transpose (fun (i : m) (j : n) => c) = fun j i => c := by
      funext i j -- the rw below does not work without this line
      rw [transpose]

source
def eqns :
Lean.ParserDescr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
opaque eqnsAttribute :
Lean.NameMapExtension (Array Lean.Name)