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

feat: lift useful binder term syntax to tactics

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-30 07:15:42 -07:00
parent 2eb330e36a
commit fc65b76331
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Parser/Tactic.lean
View file

@ -64,6 +64,13 @@ def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 ma
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
/- Term binders as tactics. They are all implemented as macros using the triad: named holes, hygiene, and `refine` tactic. -/
@[builtinTacticParser] def «have» := parser! "have " >> Term.optIdent >> termParser >> (Term.haveAssign <|> Term.fromTerm) >> "; " >> tacticParser
@[builtinTacticParser] def «suffices» := parser! "suffices " >> Term.optIdent >> termParser >> Term.fromTerm >> "; " >> tacticParser
@[builtinTacticParser] def «show» := parser! "show " >> termParser >> " from " >> tacticParser
@[builtinTacticParser] def «let» := parser! "let " >> Term.letDecl >> "; " >> tacticParser
@[builtinTacticParser] def «let!» := parser! "let! " >> Term.letDecl >> "; " >> tacticParser
end Tactic
end Parser
end Lean