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: Lean.Meta.NormCast.Label

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

• move: Lean.Meta.NormCast.Label

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

• squash: Lean.Meta.NormCast.Label

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

instance Lean.Meta.NormCast.instDecidableEqLabel : DecidableEq Lean.Meta.NormCast.Label

Equations

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

instance Lean.Meta.NormCast.instReprLabel : Repr Lean.Meta.NormCast.Label

Equations

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

instance Lean.Meta.NormCast.instInhabitedLabel : Inhabited Lean.Meta.NormCast.Label

Equations

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

def Lean.Meta.NormCast.getSimpArgs (e : Lean.Expr) : Lean.MetaM (Array Lean.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 : Lean.Expr) : Lean.MetaM Nat

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

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

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

def Lean.Meta.NormCast.countInternalCoes (e : Lean.Expr) : Lean.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 : Lean.Expr) : Lean.MetaM Lean.Meta.NormCast.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 : Lean.Meta.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 : Lean.Meta.SimpExtension

  A simp set which lifts coercions to the top level.

• down : Lean.Meta.SimpExtension

  A simp set which pushes coercions to the leaves.

• squash : Lean.Meta.SimpExtension

  A simp set which simplifies transitive coercions.

instance Lean.Meta.NormCast.instInhabitedNormCastExtension : Inhabited Lean.Meta.NormCast.NormCastExtension

Equations

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

opaque Lean.Meta.NormCast.normCastExt : Lean.Meta.NormCast.NormCastExtension

The norm_cast extension data.

def Lean.Meta.NormCast.addElim (decl : Lake.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.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 : Lake.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.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 : Lake.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.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 : Lake.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.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.