inductive Lean.Meta.NormCast.Label : Type

Label is a type used to classify norm_cast lemmas.

• elim lemma: LHS has 0 head coes and ≥ 1 internal coe
• move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
• squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

• elim : Label

  elim lemma: LHS has 0 head coes and ≥ 1 internal coe

• move : Label

  move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes

• squash : Label

  squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

instance Lean.Meta.NormCast.instDecidableEqLabel : DecidableEq Label

instance Lean.Meta.NormCast.instReprLabel : Repr Label

instance Lean.Meta.NormCast.instInhabitedLabel : Inhabited Label

def Lean.Meta.NormCast.getSimpArgs (e : Expr) : MetaM (Array Expr)

Assuming e is an application, returns the list of subterms that simp will rewrite in.

partial def Lean.Meta.NormCast.countHeadCoes (e : Expr) : MetaM Nat

Counts how many coercions are at the head of the expression.

partial def Lean.Meta.NormCast.countCoes (e : Expr) : MetaM Nat

Counts how many coercions are inside the expression, including the head ones.

def Lean.Meta.NormCast.countInternalCoes (e : Expr) : MetaM Nat

Counts how many coercions are inside the expression, excluding the head ones.

def Lean.Meta.NormCast.classifyType (ty : Expr) : MetaM Label

Classifies a declaration of type ty as a norm_cast rule.

opaque Lean.Meta.NormCast.pushCastExt : SimpExtension

The push_cast simp attribute.

structure Lean.Meta.NormCast.NormCastExtension : Type

The norm_cast attribute stores a simp set for each of the three types of norm_cast lemma.

• up : SimpExtension

  A simp set which lifts coercions to the top level.

• down : SimpExtension

  A simp set which pushes coercions to the leaves.

• squash : SimpExtension

  A simp set which simplifies transitive coercions.

instance Lean.Meta.NormCast.instInhabitedNormCastExtension : Inhabited NormCastExtension

opaque Lean.Meta.NormCast.normCastExt : NormCastExtension

The norm_cast extension data.

def Lean.Meta.NormCast.addElim (decl : Name) (kind : AttributeKind := AttributeKind.global) (prio : Nat := 1000) : MetaM Unit

addElim decl adds decl as an elim lemma to be used by norm_cast.

def Lean.Meta.NormCast.addMove (decl : Name) (kind : AttributeKind := AttributeKind.global) (prio : Nat := 1000) : MetaM Unit

addMove decl adds decl as a move lemma to be used by norm_cast.

def Lean.Meta.NormCast.addSquash (decl : Name) (kind : AttributeKind := AttributeKind.global) (prio : Nat := 1000) : MetaM Unit

addSquash decl adds decl as a squash lemma to be used by norm_cast.

def Lean.Meta.NormCast.addInfer (decl : Name) (kind : AttributeKind := AttributeKind.global) (prio : Nat := 1000) : MetaM Unit

addInfer decl infers the label of decl (elim, move, or squash) and arranges for it to be used by norm_cast.

• elim lemma: LHS has 0 head coes and ≥ 1 internal coe
• move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
• squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes