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

chore: fix Notation.lean

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-21 09:47:11 -08:00
parent 9dfb840c8a
commit c43e77d1a5
1 changed files with 50 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

100
src/Init/Notation.lean
View file

@ -12,11 +12,11 @@ import Init.Prelude
namespace Lean.Parser.Syntax
syntax:65 [addPrec] prec " + " prec:66 : prec
syntax:65 [subPrec] prec " - " prec:66 : prec
syntax:65 (name := addPrec) prec " + " prec:66 : prec
syntax:65 (name := subPrec) prec " - " prec:66 : prec
syntax:65 [addPrio] prio " + " prio:66 : prio
syntax:65 [subPrio] prio " - " prio:66 : prio
syntax:65 (name := addPrio) prio " + " prio:66 : prio
syntax:65 (name := subPrio) prio " - " prio:66 : prio
end Lean.Parser.Syntax
@ -54,7 +54,7 @@ macro:max x:stx ",+,?" : stx => `(stx| sepBy1($x, ",", ", ", allowTrailingSep))
macro "!" x:stx : stx => `(stx| notFollowedBy($x))
syntax[rawNatLit] "natLit! " num : term
syntax (name := rawNatLit) "natLit! " num : term
infixr:90 " ∘ " => Function.comp
infixr:35 " × " => Prod
@ -160,28 +160,28 @@ macro_rules
namespace Parser.Tactic
syntax[intro] "intro " notFollowedBy("|") (colGt term:max)* : tactic
syntax[intros] "intros " (colGt (ident <|> "_"))* : tactic
syntax[revert] "revert " (colGt ident)+ : tactic
syntax[clear] "clear " (colGt ident)+ : tactic
syntax[subst] "subst " (colGt ident)+ : tactic
syntax[assumption] "assumption" : tactic
syntax[apply] "apply " term : tactic
syntax[exact] "exact " term : tactic
syntax[refine] "refine " term : tactic
syntax[refine!] "refine! " term : tactic
syntax[case] "case " ident " => " tacticSeq : tactic
syntax[allGoals] "allGoals " tacticSeq : tactic
syntax[focus] "focus " tacticSeq : tactic
syntax[skip] "skip" : tactic
syntax[done] "done" : tactic
syntax[traceState] "traceState" : tactic
syntax[failIfSuccess] "failIfSuccess " tacticSeq : tactic
syntax[generalize] "generalize " atomic(ident " : ")? term:51 " = " ident : tactic
syntax[paren] "(" tacticSeq ")" : tactic
syntax[withReducible] "withReducible " tacticSeq : tactic
syntax[withReducibleAndInstances] "withReducibleAndInstances " tacticSeq : tactic
syntax:2[orelse] tactic "<|>" tactic:1 : tactic
syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic
syntax (name := revert) "revert " (colGt ident)+ : tactic
syntax (name := clear) "clear " (colGt ident)+ : tactic
syntax (name := subst) "subst " (colGt ident)+ : tactic
syntax (name := assumption) "assumption" : tactic
syntax (name := apply) "apply " term : tactic
syntax (name := exact) "exact " term : tactic
syntax (name := refine) "refine " term : tactic
syntax (name := refine!) "refine! " term : tactic
syntax (name := case) "case " ident " => " tacticSeq : tactic
syntax (name := allGoals) "allGoals " tacticSeq : tactic
syntax (name := focus) "focus " tacticSeq : tactic
syntax (name := skip) "skip" : tactic
syntax (name := done) "done" : tactic
syntax (name := traceState) "traceState" : tactic
syntax (name := failIfSuccess) "failIfSuccess " tacticSeq : tactic
syntax (name := generalize) "generalize " atomic(ident " : ")? term:51 " = " ident : tactic
syntax (name := paren) "(" tacticSeq ")" : tactic
syntax (name := withReducible) "withReducible " tacticSeq : tactic
syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
syntax:2 (name := orelse) tactic "<|>" tactic:1 : tactic
macro "try " t:tacticSeq : tactic => `(($t) <|> skip)
@ -194,21 +194,21 @@ syntax locationTarget := "⊢" <|> "|-"
syntax locationHyp := (colGt ident)+
syntax location := withPosition("at " locationWildcard <|> locationTarget <|> locationHyp)
syntax[change] "change " term (location)? : tactic
syntax[changeWith] "change " term " with " term (location)? : tactic
syntax (name := change) "change " term (location)? : tactic
syntax (name := changeWith) "change " term " with " term (location)? : tactic
syntax rwRule := ("←" <|> "<-")? term
syntax rwRuleSeq := "[" rwRule,+,? "]"
syntax[rewrite] "rewrite " rwRule (location)? : tactic
syntax[rewriteSeq, high] "rewrite " rwRuleSeq (location)? : tactic
syntax[erewrite] "erewrite " rwRule (location)? : tactic
syntax[erewriteSeq, high] "erewrite " rwRuleSeq (location)? : tactic
syntax (name := rewrite) "rewrite " rwRule (location)? : tactic
syntax (name := rewriteSeq) (priority := high) "rewrite " rwRuleSeq (location)? : tactic
syntax (name := erewrite) "erewrite " rwRule (location)? : tactic
syntax (name := erewriteSeq) (priority := high) "erewrite " rwRuleSeq (location)? : tactic
syntax[rw] "rw " rwRule (location)? : tactic
syntax[rwSeq, high] "rw " rwRuleSeq (location)? : tactic
syntax[erw] "erw " rwRule (location)? : tactic
syntax[erwSeq, high] "erw " rwRuleSeq (location)? : tactic
syntax (name := rw) "rw " rwRule (location)? : tactic
syntax (name := rwSeq) (priority := high) "rw " rwRuleSeq (location)? : tactic
syntax (name := erw) "erw " rwRule (location)? : tactic
syntax (name := erwSeq) (priority := high) "erw " rwRuleSeq (location)? : tactic
private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
`(tactic| $tac; try (withReducible rfl))
@ -229,31 +229,31 @@ def expandERw : Macro :=
def expandERwSeq : Macro :=
fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))
syntax[injection] "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
syntax[«have»] "have " haveDecl : tactic
syntax[«suffices»] "suffices " sufficesDecl : tactic
syntax[«show»] "show " term : tactic
syntax[«let»] "let " letDecl : tactic
syntax[«let!»] "let! " letDecl : tactic
syntax[letrec] withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
syntax (name := «have») "have " haveDecl : tactic
syntax (name := «suffices») "suffices " sufficesDecl : tactic
syntax (name := «show») "show " term : tactic
syntax (name := «let») "let " letDecl : tactic
syntax (name := «let!») "let! " letDecl : tactic
syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
syntax inductionAlt := "| " (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
syntax inductionAlts := "with " withPosition( (colGe inductionAlt)+)
syntax[induction] "induction " term,+ (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic
syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic
syntax casesTarget := atomic(ident " : ")? term
syntax[cases] "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
syntax matchAlt := "| " term,+ " => " (hole <|> syntheticHole <|> tacticSeq)
syntax matchAlts := withPosition((colGe matchAlt)+)
syntax[«match»] "match " matchDiscr,+ (" : " term)? " with " matchAlts : tactic
syntax (name := «match») "match " matchDiscr,+ (" : " term)? " with " matchAlts : tactic
syntax[introMatch] "intro " matchAlts : tactic
syntax (name := introMatch) "intro " matchAlts : tactic
syntax[existsIntro] "exists " term : tactic
syntax (name := existsIntro) "exists " term : tactic
/- We use a priority > default, to avoid ambiguity with the builtin `have` notation -/
macro[high] "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
syntax "repeat " tacticSeq : tactic
macro_rules