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