Documentation
Lean
.
Meta
.
Tactic
.
Grind
.
PropagatorAttr
Search
return to top
source
Imports
Init.Grind
Lean.Meta.Tactic.Grind.Proof
Imported by
Lean
.
Meta
.
Grind
.
BuiltinPropagators
Lean
.
Meta
.
Grind
.
instInhabitedBuiltinPropagators
Lean
.
Meta
.
Grind
.
builtinPropagatorsRef
Lean
.
Meta
.
Grind
.
registerBuiltinUpwardPropagator
Lean
.
Meta
.
Grind
.
registerBuiltinDownwardPropagator
source
structure
Lean
.
Meta
.
Grind
.
BuiltinPropagators
:
Type
Builtin propagators.
up :
Std.HashMap
Name
Propagator
down :
Std.HashMap
Name
Propagator
Instances For
source
instance
Lean
.
Meta
.
Grind
.
instInhabitedBuiltinPropagators
:
Inhabited
BuiltinPropagators
Equations
Lean.Meta.Grind.instInhabitedBuiltinPropagators
=
{
default
:=
{
up
:=
default
,
down
:=
default
}
}
source
opaque
Lean
.
Meta
.
Grind
.
builtinPropagatorsRef
:
IO.Ref
BuiltinPropagators
source
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
Instances For
source
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
Instances For