Documentation

Lean.Meta.Tactic.Grind.Arith.Types

structure Lean.Meta.Grind.Arith.State :

State for the arithmetic procedures.

Instances For

instance Lean.Meta.Grind.Arith.instInhabitedState :

Inhabited State

Equations

Lean.Meta.Grind.Arith.instInhabitedState = { default := Lean.Meta.Grind.Arith.instInhabitedState.default }

def Lean.Meta.Grind.Arith.instInhabitedState.default :

Equations

Lean.Meta.Grind.Arith.instInhabitedState.default = { }

Instances For