Sebastian Ullrich
|
5955e3fce8
|
chore(library/init/lean/parser/parsec): proper namespacing
|
2018-07-12 10:35:22 +02:00 |
|
Sebastian Ullrich
|
72b255d4e1
|
chore(library/init/lean/parser/parser_t): rename module and type to parsec to avoid nested use of parser
|
2018-07-12 10:35:20 +02:00 |
|
Sebastian Ullrich
|
6fa4e56fbe
|
feat(library/init/lean/parser/syntax): add and test reprinter
|
2018-07-11 14:34:50 +02:00 |
|
Sebastian Ullrich
|
b2f9b2c180
|
feat(library/init/lean/parser/{syntax,reader}): store whitespace around tokens
|
2018-07-11 14:34:50 +02:00 |
|
Sebastian Ullrich
|
b1aff14650
|
feat(library/init/lean/parser/syntax.lean): simplify syntax debug output
|
2018-06-07 14:57:13 +02:00 |
|
Sebastian Ullrich
|
1c380037d3
|
refactor(library/init/lean/parser/syntax): replace syntax.lst with syntax.node, remove span field from syntax_node
|
2018-06-06 15:46:39 +02:00 |
|
Sebastian Ullrich
|
732c823646
|
feat(library/init/lean/parser): remove syntax_id, use De Bruijn indices instead
|
2018-06-06 15:36:28 +02:00 |
|
Leonardo de Moura
|
1bae8f8eab
|
refactor(library/init/lean/ir/parser): parser.lean => parser_t.lean
|
2018-06-05 08:00:13 -07:00 |
|
Sebastian Ullrich
|
6a0f3056f4
|
chore(library/init/lean/parser/syntax): cleanup
|
2018-06-04 11:02:45 +02:00 |
|
Leonardo de Moura
|
485b16a413
|
feat(library/init/lean/parser/syntax): use position
|
2018-04-30 16:13:01 -07:00 |
|
Leonardo de Moura
|
1b5c3c117e
|
fix(library/init/lean/parser/syntax): leanchecker error: multiple definitions of lean.parser.position
|
2018-04-30 13:44:23 -07:00 |
|
Leonardo de Moura
|
3c317a30db
|
chore(library/init/lean/parser): remove sorry warnings and init/meta dependencies
|
2018-04-30 13:38:25 -07:00 |
|
Sebastian Ullrich
|
1e53b03aa3
|
feat(init/parser): add prototype code for syntax trees, macro expansion, and name resolution
|
2018-04-27 17:57:03 +02:00 |
|