LeanSubst.Arity

source

def LeanSubst.mk0 {T : Type} :

Fin 0 → T

Equations

Instances For

source

@[simp]

theorem LeanSubst.mk0_eta {T : Type} {t : Fin 0 → T} :

t = mk0

source

def LeanSubst.mk1 {T : Type} :

T → Fin 1 → T

Equations

LeanSubst.mk1 x✝ ⟨0, isLt⟩ = x✝

Instances For

source

@[simp]

theorem LeanSubst.mk1_eta {T : Type} {t : Fin 1 → T} :

(fun (i : Fin 1) => mk1 (t 0) i) = t

source

@[simp]

theorem LeanSubst.mk1_0 {T : Type} {t : T} :

mk1 t 0 = t

source

@[simp]

theorem LeanSubst.mk1_cong {T : Type} {a1 a2 : T} :

mk1 a1 = mk1 a2 ↔ a1 = a2

source

def LeanSubst.mk2 {T : Type} :

T → T → Fin 2 → T

Equations

LeanSubst.mk2 x✝¹ x✝ ⟨0, isLt⟩ = x✝¹
LeanSubst.mk2 x✝¹ x✝ ⟨1, isLt⟩ = x✝

Instances For

source

@[simp]

theorem LeanSubst.mk2_eta {T : Type} {t : Fin 2 → T} :

(fun (i : Fin 2) => mk2 (t 0) (t 1) i) = t

source

@[simp]

theorem LeanSubst.mk2_0 {T : Type} {t1 t2 : T} :

mk2 t1 t2 0 = t1

source

@[simp]

theorem LeanSubst.mk2_1 {T : Type} {t1 t2 : T} :

mk2 t1 t2 1 = t2

source

@[simp]

theorem LeanSubst.mk2_cong {T : Type} {a1 b1 a2 b2 : T} :

mk2 a1 b1 = mk2 a2 b2 ↔ a1 = a2 ∧ b1 = b2

source

def LeanSubst.mk3 {T : Type} :

T → T → T → Fin 3 → T

Equations

LeanSubst.mk3 x✝² x✝¹ x✝ ⟨0, isLt⟩ = x✝²
LeanSubst.mk3 x✝² x✝¹ x✝ ⟨1, isLt⟩ = x✝¹
LeanSubst.mk3 x✝² x✝¹ x✝ ⟨2, isLt⟩ = x✝

Instances For

source

@[simp]

theorem LeanSubst.mk3_eta {T : Type} {t : Fin 3 → T} :

(fun (i : Fin 3) => mk3 (t 0) (t 1) (t 2) i) = t

source

@[simp]

theorem LeanSubst.mk3_0 {T : Type} {t1 t2 t3 : T} :

mk3 t1 t2 t3 0 = t1

source

@[simp]

theorem LeanSubst.mk3_1 {T : Type} {t1 t2 t3 : T} :

mk3 t1 t2 t3 1 = t2

source

@[simp]

theorem LeanSubst.mk3_2 {T : Type} {t1 t2 t3 : T} :

mk3 t1 t2 t3 2 = t3

source

@[simp]

theorem LeanSubst.mk3_cong {T : Type} {a1 b1 c1 a2 b2 c2 : T} :

mk3 a1 b1 c1 = mk3 a2 b2 c2 ↔ a1 = a2 ∧ b1 = b2 ∧ c1 = c2

source

def LeanSubst.mk4 {T : Type} :

T → T → T → T → Fin 4 → T

Equations

LeanSubst.mk4 x✝³ x✝² x✝¹ x✝ ⟨0, isLt⟩ = x✝³
LeanSubst.mk4 x✝³ x✝² x✝¹ x✝ ⟨1, isLt⟩ = x✝²
LeanSubst.mk4 x✝³ x✝² x✝¹ x✝ ⟨2, isLt⟩ = x✝¹
LeanSubst.mk4 x✝³ x✝² x✝¹ x✝ ⟨3, isLt⟩ = x✝

Instances For

source

@[simp]

theorem LeanSubst.mk4_eta {T : Type} {t : Fin 4 → T} :

(fun (i : Fin 4) => mk4 (t 0) (t 1) (t 2) (t 3) i) = t

source

@[simp]

theorem LeanSubst.mk4_0 {T : Type} {t1 t2 t3 t4 : T} :

mk4 t1 t2 t3 t4 0 = t1

source

@[simp]

theorem LeanSubst.mk4_1 {T : Type} {t1 t2 t3 t4 : T} :

mk4 t1 t2 t3 t4 1 = t2

source

@[simp]

theorem LeanSubst.mk4_2 {T : Type} {t1 t2 t3 t4 : T} :

mk4 t1 t2 t3 t4 2 = t3

source

@[simp]

theorem LeanSubst.mk4_3 {T : Type} {t1 t2 t3 t4 : T} :

mk4 t1 t2 t3 t4 3 = t4

source

@[simp]

theorem LeanSubst.mk4_cong {T : Type} {a1 b1 c1 d1 a2 b2 c2 d2 : T} :

mk4 a1 b1 c1 d1 = mk4 a2 b2 c2 d2 ↔ a1 = a2 ∧ b1 = b2 ∧ c1 = c2 ∧ d1 = d2

source

@[simp]

theorem LeanSubst.subst_mk0 {T : Type} [SubstMap T] {σ : Subst T} {x : Fin 0} :

(mk0 x)[σ] = mk0 x

source

@[simp]

theorem LeanSubst.subst_mk1 {T : Type} [SubstMap T] {σ : Subst T} {t : T} {x : Fin 1} :

(mk1 t x)[σ] = mk1 t[σ] x

source

@[simp]

theorem LeanSubst.subst_mk2 {T : Type} [SubstMap T] {σ : Subst T} {t1 t2 : T} {x : Fin 2} :

(mk2 t1 t2 x)[σ] = mk2 t1[σ] t2[σ] x

source

@[simp]

theorem LeanSubst.subst_mk3 {T : Type} [SubstMap T] {σ : Subst T} {t1 t2 t3 : T} {x : Fin 3} :

(mk3 t1 t2 t3 x)[σ] = mk3 t1[σ] t2[σ] t3[σ] x

source

@[simp]

theorem LeanSubst.subst_mk4 {T : Type} [SubstMap T] {σ : Subst T} {t1 t2 t3 t4 : T} {x : Fin 4} :

(mk4 t1 t2 t3 t4 x)[σ] = mk4 t1[σ] t2[σ] t3[σ] t4[σ] x