← Copula mathematical handbook

@[reducible, inline]

abbrev Lean.Meta.Grind.PropagatorMap : Type

Equations

• Lean.Meta.Grind.PropagatorMap = Std.HashMap Lean.Name (List Lean.Meta.Grind.Propagator)

def Lean.Meta.Grind.PropagatorMap.insert (m : PropagatorMap) (declName : Name) (p : Propagator) : PropagatorMap

Equations

• m.insert declName p = Std.HashMap.insert m declName (p :: m[declName]?.getD [])

structure Lean.Meta.Grind.BuiltinPropagators : Type

Builtin propagators.

• up : PropagatorMap
• down : PropagatorMap

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedBuiltinPropagators : Inhabited BuiltinPropagators

Equations

• Lean.Meta.Grind.instInhabitedBuiltinPropagators = { default := Lean.Meta.Grind.instInhabitedBuiltinPropagators.default }

opaque Lean.Meta.Grind.builtinPropagatorsRef : IO.Ref BuiltinPropagators

def Lean.Meta.Grind.registerBuiltinUpwardPropagator (declName : Name) (proc : Propagator) : IO Unit

Equations

• Lean.Meta.Grind.registerBuiltinUpwardPropagator declName proc = Lean.Meta.Grind.registerBuiltinPropagatorCore✝ declName true proc

def Lean.Meta.Grind.registerBuiltinDownwardPropagator (declName : Name) (proc : Propagator) : IO Unit

Equations

• Lean.Meta.Grind.registerBuiltinDownwardPropagator declName proc = Lean.Meta.Grind.registerBuiltinPropagatorCore✝ declName false proc