structure Lean.Meta.Grind.BuiltinPropagators : Type

Builtin propagators.

• up : Std.HashMap Name Propagator
• down : Std.HashMap Name Propagator

instance Lean.Meta.Grind.instInhabitedBuiltinPropagators : Inhabited BuiltinPropagators

Equations

• Lean.Meta.Grind.instInhabitedBuiltinPropagators = { default := { up := default, down := 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