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

chore: simplify let decl again

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-25 16:54:26 -08:00
parent 3759cb2b81
commit ca8d6028a1
2 changed files with 5 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/TermBinders.lean
View file

@ -305,7 +305,7 @@ let type := expandOptType ref (decl.getArg 2);
let val := decl.getArg 4;
elabLetDeclAux ref n binders type val body expectedType?
@[builtinTermElab letDecl] def elabLetDecl : TermElab :=
@[builtinTermElab «let»] def elabLetDecl : TermElab :=
fun stx expectedType? => match_syntax stx with
| `(let $id $args* := $val; $body) =>
elabLetDeclAux stx id.getId args (mkHole stx) val body expectedType?

12
src/Init/Lean/Parser/Term.lean
View file

@ -94,14 +94,10 @@ def matchAlt := parser! " | " >> sepBy1 termParser ", " >> darrow >> termParser
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracktedBinder >> optType
def letSimpleDecl : Parser := try (letIdLhs >> " := ") >> termParser
def letPatDecl : Parser := termParser >> optType >> " := " >> termParser
@[builtinTermParser] def «let» := parser! "let " >> (letSimpleDecl <|> letPatDecl) >> "; " >> termParser
def equation := matchAlt
def letEqnsDecl : Parser := letIdLhs >> many1Indent equation "equations must be indented"
@[builtinTermParser] def letEqns :=
parser! "let " >> letEqnsDecl >> "; " >> termParser
def letDecl := letSimpleDecl <|> letPatDecl <|> letEqnsDecl
def equation := matchAlt
def letEqnsDecl : Parser := letIdLhs >> many1Indent equation "equations must be indented"
def letDecl := letSimpleDecl <|> letPatDecl <|> letEqnsDecl
@[builtinTermParser] def «let» := parser! "let " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let_core» := parser! "let_core " >> termParser >> ":=" >> termParser >> "; " >> termParser