source
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

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

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

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

- Lean.Meta.NormCast.instReprLabel = { reprPrec := Lean.Meta.NormCast.instReprLabel.repr }

source
def Lean.Meta.NormCast.instReprLabel.repr :
Label → Nat → Format
Equations

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

Instances For

source
def Lean.Meta.NormCast.instInhabitedLabel.default :
Label
Equations

- Lean.Meta.NormCast.instInhabitedLabel.default = Lean.Meta.NormCast.Label.elim

Instances For

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

- Lean.Meta.NormCast.instInhabitedLabel = { default := Lean.Meta.NormCast.instInhabitedLabel.default }

source
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.

Instances For

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

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

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

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

source
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)

Instances For

source
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.

Instances For

source
opaque Lean.Meta.NormCast.pushCastExt :
SimpExtension

The `push_cast` simp attribute.

source
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

source
def Lean.Meta.NormCast.instInhabitedNormCastExtension.default :
NormCastExtension
Equations

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

Instances For

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

- Lean.Meta.NormCast.instInhabitedNormCastExtension = { default := Lean.Meta.NormCast.instInhabitedNormCastExtension.default }

source
opaque Lean.Meta.NormCast.normCastExt :
NormCastExtension

The `norm_cast` extension data.

source
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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For