max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix names

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-07 07:48:33 -08:00
parent 9482976345
commit 0031769c8b
2 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Lean/Elab/Command.lean
View file

@ -65,7 +65,7 @@ do m ← builtinCommandElabTable.get;
def declareBuiltinCommandElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
let name := `_regBuiltinCommandElab ++ declName;
let type := mkApp (mkConst `IO) (mkConst `Unit);
let val := mkAppN (mkConst `addBuiltinCommandElab) #[toExpr kind, toExpr declName, mkConst declName];
let val := mkAppN (mkConst `Lean.Elab.Command.addBuiltinCommandElab) #[toExpr kind, toExpr declName, mkConst declName];
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
match env.addAndCompile {} decl with
-- TODO: pretty print error
@ -83,7 +83,7 @@ registerAttribute {
| none => throw "unknown declaration"
| some decl =>
match decl.type with
| Expr.const `Lean.CommandElab _ _ => declareBuiltinCommandElab env kind declName
| Expr.const `Lean.Elab.Command.CommandElab _ _ => declareBuiltinCommandElab env kind declName
| _ => throw (IO.userError ("unexpected command elaborator type at '" ++ toString declName ++ "' `CommandElab` expected"))
},
applicationTime := AttributeApplicationTime.afterCompilation
@ -104,6 +104,12 @@ stx.ifNode
| none => logError stx ("command '" ++ toString k ++ "' has not been implemented"))
(fun _ => logErrorUsingCmdPos ("unexpected command"))
def getNamespace : CommandElabM Name :=
do s ← get;
match s.scopes with
| [] => pure Name.anonymous
| (sc::_) => pure sc.ns
end Command
/-

4
src/Init/Lean/Elab/Term.lean
View file

@ -52,7 +52,7 @@ do m ← builtinTermElabTable.get;
def declareBuiltinTermElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
let name := `_regBuiltinTermElab ++ declName;
let type := mkApp (mkConst `IO) (mkConst `Unit);
let val := mkAppN (mkConst `addBuiltinTermElab) #[toExpr kind, toExpr declName, mkConst declName];
let val := mkAppN (mkConst `Lean.Elab.Term.addBuiltinTermElab) #[toExpr kind, toExpr declName, mkConst declName];
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
match env.addAndCompile {} decl with
-- TODO: pretty print error
@ -70,7 +70,7 @@ registerAttribute {
| none => throw "unknown declaration"
| some decl =>
match decl.type with
| Expr.const `Lean.TermElab _ _ => declareBuiltinTermElab env kind declName
| Expr.const `Lean.Elab.Term.TermElab _ _ => declareBuiltinTermElab env kind declName
| _ => throw (IO.userError ("unexpected term elaborator type at '" ++ toString declName ++ "' `TermElab` expected"))
},
applicationTime := AttributeApplicationTime.afterCompilation