This module contains utilities for dealing with equalities between constructor applications, in particular about which fields must be the same a-priori for the equality to type check.

Users include (or will include) the injectivity theorems, the per-constructor no-confusion construction and deriving type classes lik BEq, DecidableEq or Ord.

def Lean.Meta.occursOrInType (lctx : LocalContext) (e t : Expr) : Bool

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 occurrences 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 ∧ 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

• Lean.Meta.occursOrInType lctx e t = (Lean.Expr.find? (Lean.Meta.occursOrInType.go✝ lctx e) t).isSome

def Lean.Meta.occursInCtorTypeMask (ctorName : Name) : MetaM (Array Bool)

Given a constructor, returns a mask of its fields, where true means that this field occurs in the result type of the constructor.

Equations

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

def Lean.Meta.withSharedCtorIndices {α : Type} (ctor : Expr) (k : Array Expr → Array Expr → Array Expr → Array Expr → MetaM α) : MetaM α

Given a constructor (applied to the parameters already), brings its fields into scope twice, but uses the same variable for fields that appear in the result type, so that the resulting constructor applications have the same type.

Passes to k

• the new variables
• the indices to the type class
• the fields of the first constructor application
• the fields of the second constructor application

Equations

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