Documentation
SSA
.
Experimental
.
Bits
.
SafeNativeDecide
Search
Google site search
return to top
source
Imports
Init
Lean.Meta
Lean.Meta.Tactic.Simp.BuiltinSimprocs
Imported by
tacticSafe_native_decide
source
def
tacticSafe_native_decide
:
Lean.ParserDescr
Equations
tacticSafe_native_decide
=
Lean.ParserDescr.node
`tacticSafe_native_decide
1024
(
Lean.ParserDescr.nonReservedSymbol
"safe_native_decide"
false
)
Instances For