# Documentation

## Lean.Meta.Injective

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

Returns true if e occurs either in t, or in the type of a sub-expression of t. Consider the following example:

inductive Tyₛ : Type (u+1)
| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ

inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)


When looking for fixed arguments in Tmₛ.app, if we only consider occurences in the term Tmₛ (A arg), T is considered non-fixed despite the fact that A : T -> Tyₛ. This leads to an ill-typed injectivity theorem signature:

theorem Tmₛ.app.inj {T : Type u} {A : T → Tyₛ} {a : Tmₛ (Tyₛ.SPi T A)} {arg : T} {T_1 : Type u} {a_1 : Tmₛ (Tyₛ.SPi T_1 A)} :
Tmₛ.app a arg = Tmₛ.app a_1 arg →
T = T_1 ∧ HEq a a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq


Instead of checking the type of every subterm, we only need to check the type of free variables, since free variables introduced in the constructor may only appear in the type of other free variables introduced after them.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• = ctorName ++ inj
Instances For
Equations
• = ctorName ++ `injEq
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For