| .. |
|
basic.lean
|
feat(library/init, frontends/lean): add abbreviation for abbreviation
|
2019-03-15 16:01:25 -07:00 |
|
combinators.lean
|
refactor(library/init/lean/parser/term): factor out opt_type parser
|
2018-12-06 13:23:12 +01:00 |
|
command.lean
|
feat(library/init, frontends/lean): add abbreviation for abbreviation
|
2019-03-15 16:01:25 -07:00 |
|
declaration.lean
|
fix(library/init/lean/elaborator): make sure new frontend can parse the latest core.lean
|
2019-03-18 15:47:05 -07:00 |
|
identifier.lean
|
refactor(library/init/lean/parser/parsec): make sure custom error message doesn't need to be inhabited
|
2018-10-21 10:57:23 -07:00 |
|
level.lean
|
feat(library/init, frontends/lean): add abbreviation for abbreviation
|
2019-03-15 16:01:25 -07:00 |
|
module.lean
|
feat(library/init, frontends/lean): add abbreviation for abbreviation
|
2019-03-15 16:01:25 -07:00 |
|
notation.lean
|
feat(library/init/lean/elaborator): do name preresolution just before elaboration
|
2019-01-06 15:47:54 +01:00 |
|
parsec.lean
|
feat(library/init, frontends/lean): add abbreviation for abbreviation
|
2019-03-15 16:01:25 -07:00 |
|
pratt.lean
|
perf(library/init/lean/parser): reintroduce separate syntax.ident constructor with much simpler and more efficient encoding
|
2018-11-18 16:55:04 +01:00 |
|
rec.lean
|
refactor(library/init/lean/parser/rec): use init.fix
|
2019-03-12 08:31:58 -07:00 |
|
string_literal.lean
|
feat(library/init/data/char): use uint32 instead of nat for defining char
|
2019-02-15 18:07:55 -08:00 |
|
syntax.lean
|
feat(library/init, frontends/lean): add abbreviation for abbreviation
|
2019-03-15 16:01:25 -07:00 |
|
term.lean
|
fix(library/init/lean/parser/term,frontends/lean/builtin_exprs): @& should have higher rbp than ->
|
2019-03-07 14:35:25 +01:00 |
|
token.lean
|
feat(library/init/lean,frontends/lean/vm_elaborator): set_option
|
2019-01-20 18:21:41 +01:00 |
|
trie.lean
|
refactor(library/init/data): avoid indirection at rbmap
|
2018-10-26 17:14:09 -07:00 |
