Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.Internalize

source
partial def Lean.Meta.Grind.Arith.Linear.markVars (e : Expr) :
LinearM Unit
source
def Lean.Meta.Grind.Arith.Linear.markVars.markVar (e : Expr) :
LinearM Unit
Equations
    Instances For
      source
      partial def Lean.Meta.Grind.Arith.Linear.markVars.isNumeral (e : Expr) :
      Bool
      source
      def Lean.Meta.Grind.Arith.Linear.internalize (e : Expr) (parent? : Option Expr) :
      GoalM Unit
      Equations
        Instances For