Documentation
Lean
.
Util
.
TestExtern
Search
return to top
source
Imports
Init.Notation
Lean.Exception
Lean.Compiler.ExternAttr
Lean.Compiler.ImplementedByAttr
Lean.Elab.Command
Lean.Meta.Eval
Lean.Meta.Tactic.Unfold
Imported by
Lean
.
testExternCmd
Lean
.
elabTestExtern
source
def
Lean
.
testExternCmd
:
ParserDescr
Instances For
source
unsafe def
Lean
.
elabTestExtern
:
Elab.Command.CommandElab
Instances For