Leonardo de Moura
|
3f9549485f
|
feat(frontends/lean/parser): restore config options in the end of sections/namespaces
|
2015-12-09 11:24:37 -08:00 |
|
Leonardo de Moura
|
68110faa4d
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
Leonardo de Moura
|
2be83fbff7
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
Leonardo de Moura
|
5312afa7ec
|
feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes
The new test contains examples that required explicit levels.
|
2014-11-12 10:52:32 -08:00 |
|