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

feat: add inferMod field to CtorView

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-13 15:05:16 -07:00
parent 2cc2e71a53
commit 2bf10b3d2c
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -159,8 +159,9 @@ withDeclId declId fun name => do
let ctorName := ctor.getIdAt 2;
let ctorName := declName ++ ctorName;
ctorName ← applyVisibility (ctor.getArg 2) ctorModifiers.visibility ctorName;
let inferMod := !(ctor.getArg 3).isNone;
let (binders, type?) := expandOptDeclSig (ctor.getArg 4);
pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
};
pure {
ref := decl,

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

@ -13,12 +13,13 @@ namespace Command
structure CtorView :=
(ref : Syntax)
(modifiers : Modifiers)
(inferMod : Bool) -- true if `{}` is used in the constructor declaration
(declName : Name)
(binders : Syntax)
(type? : Option Syntax)
instance CtorView.inhabited : Inhabited CtorView :=
⟨{ ref := arbitrary _, modifiers := {}, declName := arbitrary _, binders := arbitrary _, type? := none }⟩
⟨{ ref := arbitrary _, modifiers := {}, inferMod := false, declName := arbitrary _, binders := arbitrary _, type? := none }⟩
structure InductiveView :=
(ref : Syntax)