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]

def eqns : Lean.ParserDescr

Equations

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

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