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

chore: naming

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-17 09:18:20 -07:00
parent ba3f461505
commit d2f26e142d
3 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Declaration.lean
View file

@ -165,12 +165,12 @@ inductiveSyntaxToView modifiers decl 2
def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
v ← inductiveSyntaxToView modifiers stx;
elabInductiveCore #[v]
elabInductiveViews #[v]
def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
let modifiers := modifiers.addAttribute { name := `class };
v ← classInductiveSyntaxToView modifiers stx;
elabInductiveCore #[v]
elabInductiveViews #[v]
@[builtinCommandElab declaration]
def elabDeclaration : CommandElab :=
@ -213,7 +213,7 @@ views ← elems.mapM $ fun stx => do {
modifiers ← elabModifiers (stx.getArg 0);
inductiveSyntaxToView modifiers (stx.getArg 1)
};
elabInductiveCore views
elabInductiveViews views
private def isMutualPreambleCommand (stx : Syntax) : Bool :=
let k := stx.getKind;

2
src/Lean/Elab/Inductive.lean
View file

@ -485,7 +485,7 @@ views.forM fun view => do {
pure ()
}
def elabInductiveCore (views : Array InductiveView) : CommandElabM Unit := do
def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
let view0 := views.get! 0;
let ref := view0.ref;
decl ← runTermElabM view0.declName $ fun vars => mkInductiveDecl vars views;

4
src/Lean/Elab/Structure.lean
View file

@ -71,7 +71,7 @@ else do
declName ← applyVisibility ctor modifiers.visibility declName;
pure { ref := ctor, name := name, modifiers := modifiers, inferMod := inferMod, declName := declName }
private def elabStructView (view : StructView) : TermElabM ElabStructResult :=
private def elabStructureView (view : StructView) : TermElabM ElabStructResult :=
throw $ arbitrary _ -- TODO
/-
@ -102,7 +102,7 @@ withDeclId declId $ fun name => do
declName ← mkDeclName declId modifiers name;
ctor ← expandCtor stx declName;
allUserLevelNames ← getLevelNames;
r ← runTermElabM declName $ fun scopeVars => Term.elabBinders params $ fun params => elabStructView {
r ← runTermElabM declName $ fun scopeVars => Term.elabBinders params $ fun params => elabStructureView {
ref := stx,
modifiers := modifiers,
scopeLevelNames := scopeLevelNames,