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

feat: have: remove unnecessary whitespace check and allow name- and type-less have

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-25 14:24:17 +02:00
parent fb0c62d546
commit e918e39ed0
3 changed files with 16 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Lean/Elab/BuiltinNotation.lean
View file

@ -64,19 +64,17 @@ open Meta
@[builtinMacro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
let thisId := mkIdentFrom stx `this
match stx with
| `(have $x $bs* $[: $type]? := $val $[;]? $body) => `(let_fun $x $bs* $[: $type]? := $val; $body)
| `(have : $type := $val $[;]? $body) => `(have $thisId : $type := $val; $body)
| `(have $x $bs* $[: $type]? $alts:matchAlts $[;]? $body) => `(let_fun $x $bs* $[: $type]? $alts:matchAlts; $body)
| `(have : $type $alts:matchAlts $[;]? $body) => `(have $thisId : $type $alts:matchAlts; $body)
| `(have $pattern:term := $val:term $[;]? $body) => `(let_fun $pattern:term := $val:term ; $body)
| _ => Macro.throwUnsupported
| `(have $x $bs* $[: $type]? := $val $[;]? $body) => `(let_fun $x $bs* $[: $type]? := $val; $body)
| `(have $[: $type]? := $val $[;]? $body) => `(have $thisId:ident $[: $type]? := $val; $body)
| `(have $x $bs* $[: $type]? $alts:matchAlts $[;]? $body) => `(let_fun $x $bs* $[: $type]? $alts:matchAlts; $body)
| `(have $[: $type]? $alts:matchAlts $[;]? $body) => `(have $thisId:ident $[: $type]? $alts:matchAlts; $body)
| `(have $pattern:term := $val:term $[;]? $body) => `(let_fun $pattern:term := $val:term ; $body)
| _ => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro
| `(suffices $x:ident : $type from $val $[;]? $body) => `(have $x : $type := $body; $val)
| `(suffices $type:term from $val $[;]? $body) => `(have : $type := $body; $val)
| `(suffices $x:ident : $type by%$b $tac:tacticSeq $[;]? $body) => `(have $x : $type := $body; by%$b $tac:tacticSeq)
| `(suffices $type:term by%$b $tac:tacticSeq $[;]? $body) => `(have : $type := $body; by%$b $tac:tacticSeq)
| _ => Macro.throwUnsupported
| `(suffices $[$x :]? $type from $val $[;]? $body) => `(have $[$x]? : $type := $body; $val)
| `(suffices $[$x :]? $type by%$b $tac:tacticSeq $[;]? $body) => `(have $[$x]? : $type := $body; by%$b $tac:tacticSeq)
| _ => Macro.throwUnsupported
open Lean.Parser in
private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do

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

@ -168,11 +168,9 @@ def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
@[builtinTermParser] def «let_delayed» := leading_parser:leadPrec withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser
-- like `let_fun` but with optional name
def haveIdLhs := nodeWithAntiquot "haveIdLhs" `Lean.Parser.Term.haveIdLhs <| ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
def haveNoIdLhs := nodeWithAntiquot "haveNoIdLhs" `Lean.Parser.Term.haveNoIdLhs <| typeSpec
def haveLhs := haveIdLhs <|> haveNoIdLhs
def haveIdDecl := nodeWithAntiquot "haveIdDecl" `Lean.Parser.Term.haveIdDecl $ atomic (haveLhs >> " := ") >> termParser
def haveEqnsDecl := nodeWithAntiquot "haveEqnsDecl" `Lean.Parser.Term.haveEqnsDecl $ haveLhs >> matchAlts
def haveIdLhs := optional (ident >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder))) >> optType
def haveIdDecl := nodeWithAntiquot "haveIdDecl" `Lean.Parser.Term.haveIdDecl $ atomic (haveIdLhs >> " := ") >> termParser
def haveEqnsDecl := nodeWithAntiquot "haveEqnsDecl" `Lean.Parser.Term.haveEqnsDecl $ haveIdLhs >> matchAlts
def haveDecl := nodeWithAntiquot "haveDecl" `Lean.Parser.Term.haveDecl (haveIdDecl <|> letPatDecl <|> haveEqnsDecl)
@[builtinTermParser] def «have» := leading_parser:leadPrec withPosition ("have " >> haveDecl) >> optSemicolon termParser

4
tests/lean/have.lean
View file

@ -5,3 +5,7 @@ example : 5 = 3 :=
have t : True := _
have f : 5 = 6 := _
f
example : True :=
have := True.intro
this