Documentation

Lean.Meta.Tactic.Grind.PropagatorAttr

source
structure Lean.Meta.Grind.BuiltinPropagators :
Type

Builtin propagators.

Instances For
    source
    instance Lean.Meta.Grind.instInhabitedBuiltinPropagators :
    Inhabited BuiltinPropagators
    Equations
      source
      opaque Lean.Meta.Grind.builtinPropagatorsRef :
      IO.Ref BuiltinPropagators
      source
      def Lean.Meta.Grind.registerBuiltinUpwardPropagator (declName : Name) (proc : Propagator) :
      IO Unit
      Equations
        Instances For
          source
          def Lean.Meta.Grind.registerBuiltinDownwardPropagator (declName : Name) (proc : Propagator) :
          IO Unit
          Equations
            Instances For