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

chore: remove optional partial from 'let rec'

Browse source 
It will inherit the parent declaration annotation.
This commit is contained in:
Leonardo de Moura 2020-09-02 13:18:45 -07:00
parent a8f8be4b30
commit 0883f96da0
2 changed files with 5 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/Elab/LetRec.lean
View file

@ -18,30 +18,20 @@ structure LetRecDeclView :=
structure LetRecView :=
(ref : Syntax)
(isPartial : Bool)
(decls : Array LetRecDeclView)
(body : Syntax)
private def mkLetRecView (letRec : Syntax) : LetRecView :=
let decls := (letRec.getArg 2).getArgs.getSepElems.map fun attrDeclSyntax =>
let decls := (letRec.getArg 1).getArgs.getSepElems.map fun attrDeclSyntax =>
{ attrs := attrDeclSyntax.getArg 0, decl := (attrDeclSyntax.getArg 1).getArg 0 : LetRecDeclView };
{ decls := decls,
ref := letRec,
isPartial := !(letRec.getArg 1).isNone,
body := letRec.getArg 4 }
body := letRec.getArg 3 }
def LetRecView.review (view : LetRecView) : Syntax :=
let result := view.ref;
let result := result.setArg 4 view.body;
let result :=
if view.isPartial then
if (result.getArg 1).isNone then
result.setArg 1 (mkNullNode #[mkAtomFrom result "partial "])
else
result
else
result.setArg 1 mkNullNode;
let result := result.setArg 2 $ mkSepStx
let result := result.setArg 3 view.body;
let result := result.setArg 1 $ mkSepStx
(view.decls.map fun decl => mkNullNode #[decl.attrs, mkNode `Lean.Parser.Term.letDecl #[decl.decl]])
(mkAtomFrom result ", ");
result

2
src/Lean/Parser/Term.lean
View file

@ -133,7 +133,7 @@ def attrArg : Parser := ident <|> strLit <|> numLit
def attrInstance := parser! rawIdent >> many attrArg
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
@[builtinTermParser] def «letrec» :=
parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> optional ("partial ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
def leftArrow : Parser := unicodeSymbol " ← " " <- "
def doLet := parser! "let ">> letDecl