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

feat: modifiers for 'let rec's

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-05 06:48:26 -07:00
parent 19be535fb3
commit 0d39c00782
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Elab/MutualDef.lean
View file

@ -500,7 +500,7 @@ mainHeaders.size.foldM
})
preDecls
def pushLetRecs (preDecls : Array PreDeclaration) (letRecClosures : List LetRecClosure) (kind : DefKind) : Array PreDeclaration :=
def pushLetRecs (preDecls : Array PreDeclaration) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : Array PreDeclaration :=
letRecClosures.foldl
(fun (preDecls : Array PreDeclaration) (c : LetRecClosure) =>
let type := Closure.mkForall c.localDecls c.toLift.type;
@ -508,7 +508,7 @@ letRecClosures.foldl
preDecls.push {
kind := kind,
declName := c.toLift.declName,
modifiers := { attrs := c.toLift.attrs },
modifiers := { modifiers with attrs := c.toLift.attrs },
type := type,
val := val
})
@ -518,6 +518,11 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
if mainHeaders.any fun h => h.kind.isTheorem then DefKind.«theorem»
else DefKind.«def»
def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers :=
{ isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable,
isPartial := mainHeaders.any fun h => h.modifiers.isPartial,
isUnsafe := mainHeaders.any fun h => h.modifiers.isUnsafe }
/-
- `sectionVars`: The section variables used in the `mutual` block.
- `mainHeaders`: The elaborated header of the top-level definitions being defined by the mutual block.
@ -549,7 +554,8 @@ let mainVals := mainVals.map r.apply;
let mainHeaders := mainHeaders.map fun h => { h with type := r.apply h.type };
let letRecClosures := letRecClosures.map fun c => { c with toLift := { c.toLift with type := r.apply c.toLift.type, val := r.apply c.toLift.val } };
let letRecKind := getKindForLetRecs mainHeaders;
pushMain (pushLetRecs #[] letRecClosures letRecKind) sectionVars mainHeaders mainVals
let letRecMods := getModifiersForLetRecs mainHeaders;
pushMain (pushLetRecs #[] letRecClosures letRecKind letRecMods) sectionVars mainHeaders mainVals
end MutualClosure