Documentation

Lean.Meta.Tactic.Grind.PropagatorAttr

source
@[reducible, inline]
abbrev Lean.Meta.Grind.PropagatorMap :
Type
Instances For
    source
    def Lean.Meta.Grind.PropagatorMap.insert (m : PropagatorMap) (declName : Name) (p : Propagator) :
    PropagatorMap
    Instances For
      source
      structure Lean.Meta.Grind.BuiltinPropagators :
      Type

      Builtin propagators.

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