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

feat: add missing parsers

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-02 15:18:12 -07:00
parent 4df9983843
commit a8b434f93d
1 changed files with 13 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Conv.lean
View file

@ -16,17 +16,28 @@ syntax convSeq1Indented := withPosition((group(colGe conv ";"?))+)
syntax convSeqBracketed := "{" (group(conv ";"?))+ "}"
syntax convSeq := convSeq1Indented <|> convSeqBracketed
syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
syntax (name := skip) "skip " : conv
syntax (name := lhs) "lhs" : conv
syntax (name := rhs) "rhs" : conv
syntax (name := whnf) "whnf" : conv
syntax (name := congr) "congr" : conv
syntax (name := arg) "arg " num : conv
syntax (name := trace) "trace" : conv
syntax (name := funext) "funext" ident* : conv
syntax (name := change) "change " term : conv
syntax (name := rewrite) "rewrite " rwRuleSeq : conv
syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
syntax (name := nestedTactic) "tactic " tacticSeq : conv
syntax (name := nestedConv) convSeqBracketed : conv
syntax (name := paren) "(" convSeq ")" : conv
/-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
macro "rw " s:rwRuleSeq : conv => `(rewrite $s:rwRuleSeq)
macro "args" : conv => `(congr)
macro "left" : conv => `(lhs)
macro "right" : conv => `(rhs)
end Lean.Parser.Tactic.Conv