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

Instances For

• Lean.Meta.NormCast.instInhabitedLabel
• Lean.Meta.NormCast.instReprLabel

instance Lean.Meta.NormCast.instDecidableEqLabel : DecidableEq Label

Equations

• Lean.Meta.NormCast.instDecidableEqLabel x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.Meta.NormCast.instReprLabel : Repr Label

Equations

• Lean.Meta.NormCast.instReprLabel = { reprPrec := Lean.Meta.NormCast.reprLabel✝ }

instance Lean.Meta.NormCast.instInhabitedLabel : Inhabited Label

Equations

• Lean.Meta.NormCast.instInhabitedLabel = { default := Lean.Meta.NormCast.Label.elim }

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.

Equations

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

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.

Equations

• Lean.Meta.NormCast.countInternalCoes e = do let __do_lift ← Lean.Meta.NormCast.countCoes e let __do_lift_1 ← Lean.Meta.NormCast.countHeadCoes e pure (__do_lift - __do_lift_1)

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

Classifies a declaration of type ty as a norm_cast rule.

Equations

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

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.

Instances For

• Lean.Meta.NormCast.instInhabitedNormCastExtension

instance Lean.Meta.NormCast.instInhabitedNormCastExtension : Inhabited NormCastExtension

Equations

• Lean.Meta.NormCast.instInhabitedNormCastExtension = { default := { up := default, down := default, squash := default } }

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.

Equations

• Lean.Meta.NormCast.addElim decl kind prio = Lean.Meta.addSimpTheorem Lean.Meta.NormCast.normCastExt.up decl true false kind prio

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.

Equations

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

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.

Equations

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

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

Equations

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