feat(library/init/lean/elaborator): add skeletons

This commit is contained in:
Leonardo de Moura 2019-08-14 14:13:16 -07:00
parent e0a781063a
commit 46a2e6f311
2 changed files with 10 additions and 0 deletions

View file

@ -188,6 +188,11 @@ fun _ => do
| Except.ok env => setEnv env
| Except.error ex => logElabException (ElabException.kernel ex)
@[builtinCommandElab «variable»] def elabVariable : CommandElab :=
fun n => do
runIO (IO.println n.val);
pure ()
@[builtinCommandElab «resolve_name»] def elabResolveName : CommandElab :=
fun n => do
let id := n.getIdAt 1;

View file

@ -38,5 +38,10 @@ partial def elabTermAux : Syntax Expr → Option Expr → Bool → Elab (Syntax
def elabTerm (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab (Syntax Expr) :=
elabTermAux stx expectedType false
@[builtinTermElab «list»] def elabList : TermElab :=
fun stx _ => do
runIO (IO.println stx.val);
pure stx.val
end Elab
end Lean