TorchLean API

Docs Home Guide Examples Graphs

Lean.Meta.Tactic.Grind.Order.Internalize

Declaration colors

deftheoremstructureaxiom

Imports

Init.Grind.Order
Init.Data.Int.OfNat
Init.Grind.Module.Envelope
Lean.Meta.Tactic.Grind.Order.Assert
Lean.Meta.Tactic.Grind.Order.OrderM
Lean.Meta.Tactic.Grind.Order.Proof
Lean.Meta.Tactic.Grind.Order.StructId
Lean.Meta.Tactic.Grind.Order.Util
Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat

Imported by

Lean.Meta.Grind.Order.internalize

def Lean.Meta.Grind.Order.internalize (e : Expr) (parent? : Option Expr) :

Instances For