def Tactic.NormCast.proveEqUsing (s : Lean.Meta.SimpTheorems) (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM (Option Lean.Meta.Simp.Result)

Prove a = b using the given simp set.

Equations

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

def Tactic.NormCast.proveEqUsingDown (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM (Option Lean.Meta.Simp.Result)

Prove a = b by simplifying using move and squash lemmas.

Equations

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

def Tactic.NormCast.mkCoe (e : Lean.Expr) (ty : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Tactic.NormCast.mkCoe e ty = do let __discr ← Lean.Meta.coerce? e ty match __discr with | Lean.LOption.some e' => pure e' | x => failure

def Tactic.NormCast.isCoeOf? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def Tactic.NormCast.isNumeral? (e : Lean.Expr) : Option (Lean.Expr × Nat)

Equations

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

def Tactic.NormCast.splittingProcedure (expr : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

This is the main heuristic used alongside the elim and move lemmas. The goal is to help casts move past operators by adding intermediate casts. An expression of the shape: op (↑(x : α) : γ) (↑(y : β) : γ) is rewritten to: op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ) when (↑(↑(x : α) : β) : γ) = (↑(x : α) : γ) can be proven with a squash lemma

Equations

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

def Tactic.NormCast.prove (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

Discharging function used during simplification in the "squash" step.

TODO: normCast takes a list of expressions to use as lemmas for the discharger TODO: a tactic to print the results the discharger fails to prove

Equations

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

def Tactic.NormCast.upwardAndElim (up : Lean.Meta.SimpTheorems) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Core rewriting function used in the "squash" step, which moves casts upwards and eliminates them.

It tries to rewrite an expression using the elim and move lemmas. On failure, it calls the splitting procedure heuristic.

Equations

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

def Tactic.NormCast.numeralToCoe (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

If possible, rewrite (n : α) to (Nat.cast n : α) where n is a numeral and α ≠ ℕ. Returns a pair of the new expression and proof that they are equal.

Equations

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

def Tactic.NormCast.derive (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

The core simplification routine of normCast.

Equations

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

def Tactic.NormCast.termMod_cast_ : Lean.ParserDescr

Equations

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

def Tactic.NormCast.normCastTarget : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Tactic.NormCast.normCastHyp (fvarId : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Tactic.NormCast.tacticNorm_cast0_ : Lean.ParserDescr

Equations

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

def Tactic.NormCast.tacticAssumption_mod_cast : Lean.ParserDescr

assumption_mod_cast runs norm_cast on the goal. For each local hypothesis h, it also normalizes h and tries to use that to close the goal.

Equations

• Tactic.NormCast.tacticAssumption_mod_cast = Lean.ParserDescr.node `Tactic.NormCast.tacticAssumption_mod_cast 1024 (Lean.ParserDescr.nonReservedSymbol "assumption_mod_cast" false)

def Tactic.NormCast.tacticNorm_cast_ : Lean.ParserDescr

Normalize casts at the given locations by moving them "upwards".

Equations

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

def Tactic.NormCast.tacticRw_mod_cast___ : Lean.ParserDescr

Rewrite with the given rules and normalize casts between steps.

Equations

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

def Tactic.NormCast.tacticExact_mod_cast_ : Lean.ParserDescr

Normalize the goal and the given expression, then close the goal with exact.

Equations

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

def Tactic.NormCast.tacticApply_mod_cast_ : Lean.ParserDescr

Normalize the goal and the given expression, then apply the expression to the goal.

Equations

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

def Tactic.NormCast.convNormCast : Lean.ParserDescr

Equations

• Tactic.NormCast.convNormCast = Lean.ParserDescr.node `Tactic.NormCast.convNormCast 1024 (Lean.ParserDescr.nonReservedSymbol "norm_cast" false)

def Tactic.NormCast.evalConvNormCast : Lean.Elab.Tactic.Tactic

Equations

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

def Tactic.NormCast.pushCast : Lean.ParserDescr

Equations

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

def Tactic.NormCast.evalPushCast : Lean.Elab.Tactic.Tactic

Equations

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