max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Parser
History
Gabriel Ebner ee9c9b1312 feat: skip final newline in sepByIndent format
2022-09-18 16:43:23 -07:00
..
Attr.lean feat: add specialize attribute parser 2022-09-07 14:50:29 -07:00
Basic.lean chore: import reductions 2022-09-15 14:02:38 -07:00
Command.lean feat: move docstring before | in ctors 2022-09-14 08:26:17 -07:00
Do.lean chore: inheritDoc misbehaves on built-in parsers 2022-09-13 03:08:23 -07:00
Extension.lean chore: import reductions 2022-09-15 14:02:38 -07:00
Extra.lean feat: skip final newline in sepByIndent format 2022-09-18 16:43:23 -07:00
Level.lean chore: use Category declarations for builtin cats too (#1400) 2022-08-03 18:10:54 -07:00
Module.lean feat: strengthen pp* signatures 2022-07-03 19:14:49 +02:00
StrInterpolation.lean refactor: make String.Pos opaque 2022-03-20 10:47:13 -07:00
Syntax.lean chore: import reductions 2022-09-15 14:02:38 -07:00
Tactic.lean chore: revert marking internal notes as parser/elab docstrings 2022-08-31 17:49:43 -07:00
Term.lean feat: use sepBy1Indent for tactic blocks 2022-09-18 16:43:23 -07:00