source
structure Lean.Meta.Grind.Arith.State :
Type

State for the arithmetic procedures.

Instances For

source
def Lean.Meta.Grind.Arith.instInhabitedState.default :
State
Equations

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

Instances For

source
instance Lean.Meta.Grind.Arith.instInhabitedState :
Inhabited State
Equations

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