Documentation

Lean.Meta.Tactic.Grind.PropagatorAttr

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

          Builtin propagators.

          Instances For
            source
            instance Lean.Meta.Grind.instInhabitedBuiltinPropagators :
            Inhabited BuiltinPropagators
            Equations
              source
              def Lean.Meta.Grind.instInhabitedBuiltinPropagators.default :
              BuiltinPropagators
              Equations
                Instances For
                  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