max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Leonardo de Moura 029510d4f5 feat: syntax for setting allowTrailingSep 
@Kha This commit allows us to set `allowTrailingSep` for `sepBy` and
`sepBy1` from the `syntax` command.
```lean
syntax "[" (sepBy (allowTrailingSep := true) term ",") "]" : term
```
The new syntax is a bit verbose :)
What do you think? Any suggestions?
2020-11-08 08:12:54 -08:00
..
Compiler chore: use mut 2020-11-07 17:32:13 -08:00
Data chore: use mut 2020-11-07 17:32:13 -08:00
Elab feat: syntax for setting allowTrailingSep 2020-11-08 08:12:54 -08:00
Meta chore: use mut 2020-11-07 17:32:13 -08:00
Parser feat: syntax for setting allowTrailingSep 2020-11-08 08:12:54 -08:00
ParserCompiler fix: fix pretty printers for imported ParserDescrs 2020-11-07 17:05:07 +01:00
PrettyPrinter feat: add allowTrailingSep parameter to ParserDescr.sepBy and ParserDescr.sepBy1 2020-11-08 07:51:10 -08:00
Server chore: remove old frontend leftovers 2020-10-26 09:08:07 -07:00
Util chore: adjust files and tests 2020-11-07 17:32:12 -08:00
Attributes.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
AuxRecursor.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Class.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Compiler.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
CoreM.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Declaration.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Delaborator.lean chore: use mut 2020-11-07 17:32:13 -08:00
Elab.lean chore: remove StrategyAttrs 2020-11-02 06:39:21 -08:00
Environment.lean chore: use mut 2020-11-07 17:32:13 -08:00
Eval.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Exception.lean chore: adjust files and tests 2020-11-07 17:32:12 -08:00
Expr.lean chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
HeadIndex.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Hygiene.lean chore: cleanup 2020-10-28 09:33:19 -07:00
InternalExceptionId.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
KeyedDeclsAttribute.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Level.lean chore: cleanup 2020-10-29 10:24:16 -07:00
LocalContext.lean chore: cleanup 2020-11-05 13:17:42 -08:00
Message.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
Meta.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
MetavarContext.lean chore: use mut 2020-11-07 17:32:13 -08:00
Modifiers.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
MonadEnv.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Parser.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
ParserCompiler.lean feat: add allowTrailingSep parameter to ParserDescr.sepBy and ParserDescr.sepBy1 2020-11-08 07:51:10 -08:00
PrettyPrinter.lean fix: fix pretty printers for imported ParserDescrs 2020-11-07 17:05:07 +01:00
ProjFns.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
ReducibilityAttrs.lean refactor: add polymorphic methods for updating/querying reducibility status 2020-10-26 17:07:28 -07:00
ResolveName.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Runtime.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Server.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
Structure.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Syntax.lean chore: use Subarray combinators 2020-10-28 19:52:59 -07:00
ToExpr.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Util.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00