structure Lean.Meta.Grind.BuiltinPropagators : Type

Builtin propagators.

• up : Std.HashMap Lean.Name Lean.Meta.Grind.Propagator
• down : Std.HashMap Lean.Name Lean.Meta.Grind.Propagator

instance Lean.Meta.Grind.instInhabitedBuiltinPropagators : Inhabited Lean.Meta.Grind.BuiltinPropagators

Equations

• Lean.Meta.Grind.instInhabitedBuiltinPropagators = { default := { up := default, down := default } }

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

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

Equations

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

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

Equations

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