max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Parser
History
Leonardo de Moura ef2d9b4d59 feat: add ensureExpectedType! parser
2020-10-06 09:31:21 -07:00
..
Basic.lean chore: remove nodeSepBy1Unbox combinator 2020-10-06 08:28:40 -07:00
Command.lean feat: add notFollowedByCategoryToken parser 2020-09-26 15:53:23 -07:00
Do.lean chore: group many elements 2020-10-06 06:43:19 -07:00
Extension.lean fix: ignore $ at notFollowedByCategoryToken when inside quotations 2020-09-26 17:57:26 -07:00
Level.lean chore: universe-+ spacing 2020-09-17 08:12:28 -07:00
Module.lean feat: try to improve weird error message 2020-09-21 18:29:01 -07:00
Syntax.lean chore: use Tactic.seq1 instead of Tactic.tacticSeq1Indented 2020-10-06 08:28:41 -07:00
Tactic.lean feat: add focus tactic parser 2020-09-28 17:11:00 -07:00
Term.lean feat: add ensureExpectedType! parser 2020-10-06 09:31:21 -07:00
Transform.lean chore: Lean.Parser.Parser ~> Lean.Parser.Basic 2020-08-13 18:44:13 +02:00