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

feat: optional := before constructors in the inductive command

Browse source 
@Kha In the documentation, I will always use `:=`. The idea is to
avoid the issue: why does `structure` have a `:=` but `inductive`
doesn't.
This commit is contained in:
Leonardo de Moura 2020-11-19 06:43:14 -08:00
parent 7ccb996df5
commit 0fcf6217ec
2 changed files with 9 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -86,17 +86,15 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
/-
parser! "inductive " >> declId >> optDeclSig >> many ctor
parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
Remark: numTokens == 1 for regular `inductive` and 2 for `class inductive`.
parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor
-/
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTokens := 1) : CommandElabM InductiveView := do
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
checkValidInductiveModifier modifiers
let (binders, type?) := expandOptDeclSig decl[numTokens + 1]
let declId := decl[numTokens]
let (binders, type?) := expandOptDeclSig decl[2]
let declId := decl[1]
let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
let ctors ← decl[numTokens + 2].getArgs.mapM fun ctor => withRef ctor do
let ctors ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-- def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
let ctorModifiers ← elabModifiers ctor[1]
if ctorModifiers.isPrivate && modifiers.isPrivate then
@ -122,7 +120,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTo
}
private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
inductiveSyntaxToView modifiers decl 2
inductiveSyntaxToView modifiers decl
def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
let v ← inductiveSyntaxToView modifiers stx

4
src/Lean/Parser/Command.lean
View file

@ -47,8 +47,8 @@ def «axiom» := parser! "axiom " >> declId >> declSig
def «example» := parser! "example " >> declSig >> declVal
def inferMod := parser! atomic ("{" >> "}")
def ctor := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many ctor
def classInductive := parser! atomic ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
def classInductive := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor
def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"