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

feat: optional ; in terms

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-28 16:38:56 -07:00
parent 32349ba4e0
commit e10edde5cd
3 changed files with 19 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -79,9 +79,9 @@ def optIdent : Parser := optional (try (ident >> " : "))
def fromTerm := parser! " from " >> termParser
def haveAssign := parser! " := " >> termParser
def haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
@[builtinTermParser] def «have» := parser!:leadPrec "have " >> haveDecl >> "; " >> termParser
@[builtinTermParser] def «have» := parser!:leadPrec withPosition ("have " >> haveDecl) >> optional "; " >> termParser
def sufficesDecl := optIdent >> termParser >> fromTerm
@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> sufficesDecl >> "; " >> termParser
@[builtinTermParser] def «suffices» := parser!:leadPrec withPosition ("suffices " >> sufficesDecl) >> optional "; " >> termParser
@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
@ -156,14 +156,15 @@ def letPatDecl := node `Lean.Parser.Term.letPatDecl $ try (termParser >> pushN
def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false
-- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
@[builtinTermParser] def «let» := parser!:leadPrec "let " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let!» := parser!:leadPrec "let! " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optional "; " >> termParser
@[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optional "; " >> termParser
def attrArg : Parser := ident <|> strLit <|> numLit
-- use `rawIdent` because of attribute names such as `instance`
def attrInstance := parser! rawIdent >> many attrArg
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
@[builtinTermParser] def «letrec» :=
parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", ")
>> optional "; " >> termParser
@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser maxPrec
@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec
@ -197,6 +198,7 @@ stx.isAntiquot || stx.isIdent
@[builtinTermParser] def dollar := tparser!:0 try (dollarSymbol >> checkWsBefore "expected space") >> termParser 0
@[builtinTermParser] def dollarProj := tparser!:0 " $. " >> (fieldIdx <|> ident)
-- TODO: fix
@[builtinTermParser] def «where» := tparser!:0 " where " >> sepBy1 letDecl (group ("; " >> symbol " where "))
@[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90
@ -249,8 +251,8 @@ stx.isAntiquot || stx.isIdent
@[builtinTermParser] def panic := parser!:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
@[builtinTermParser] def dbgTrace := parser!:leadPrec "dbgTrace! " >> termParser >> "; " >> termParser
@[builtinTermParser] def assert := parser!:leadPrec "assert! " >> termParser >> "; " >> termParser
@[builtinTermParser] def dbgTrace := parser!:leadPrec withPosition ("dbgTrace! " >> termParser) >> optional "; " >> termParser
@[builtinTermParser] def assert := parser!:leadPrec withPosition ("assert! " >> termParser) >> optional "; " >> termParser
@[builtinTermParser] def «return» := parser!:leadPrec "return " >> termParser
end Term

6
tests/lean/run/def7.lean
View file

@ -39,6 +39,8 @@ theorem L.appendNil {α} : (as : L α) → append as nil = as
| nil => rfl
| cons a as =>
show cons a (fun _ => append (as ()) nil) = cons a as from
have ih : append (as ()) nil = as () from appendNil $ as ();
have thunkAux : (fun _ => as ()) = as from funext fun x => by { cases x; exact rfl };
have ih : append (as ()) nil = as () from appendNil $ as ()
have thunkAux : (fun _ => as ()) = as from funext fun x => by
cases x
exact rfl
by rw [ih, thunkAux]; exact rfl

12
tests/lean/run/newfrontend1.lean
View file

@ -95,7 +95,7 @@ by {
intro h1; intro _; intro h3;
refine! Eq.trans ?pre ?post;
exact y;
{ exact h3 };
{ exact h3 }
{ exact h1 }
}
@ -355,17 +355,17 @@ fun h1 _ h3 =>
theorem simple22 (x y z : Nat) : y = z → y = x → id (x = z + 0) :=
fun h1 h2 => show x = z + 0 by
apply Eq.trans;
exact h2.symm;
assumption;
apply Eq.trans
exact h2.symm
assumption
skip
theorem simple23 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have x = y by { apply Eq.symm; assumption };
have x = y by apply Eq.symm; assumption
Eq.trans this (by assumption)
theorem simple24 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have h : x = y by { apply Eq.symm; assumption };
have h : x = y by apply Eq.symm; assumption
Eq.trans h (by assumption)