Leonardo de Moura
|
89f62edaf0
|
refactor(library): reduce dependecies on old code, simplify normalize module
|
2016-09-19 22:12:34 -07:00 |
|
Leonardo de Moura
|
96fa8856bc
|
feat(library/equations_compiler): add mk_nonrec
|
2016-09-08 14:09:05 -07:00 |
|
Leonardo de Moura
|
c9cee9a702
|
feat(library/equations_compiler): add flag indicating whether we are compiling a lemma or not
|
2016-09-06 15:09:54 -07:00 |
|
Leonardo de Moura
|
a0b8766ffb
|
refactor(library): merge exception modules
|
2016-09-06 09:12:26 -07:00 |
|
Leonardo de Moura
|
001991dbeb
|
feat(frontends/lean): use equations_header
|
2016-08-30 13:45:59 -07:00 |
|
Leonardo de Moura
|
150ad5d292
|
feat(frontends/lean/elaborator): elaborate convoy idiom
|
2016-08-13 20:51:42 -07:00 |
|
Leonardo de Moura
|
917888a19c
|
feat(library/equations_compiler/equations): add extra data to equations macro
|
2016-08-13 12:40:02 -07:00 |
|
Leonardo de Moura
|
09459c0d84
|
refactor(library/equations_compiler): isolate old equations compiler
|
2016-08-11 10:08:30 -07:00 |
|
Leonardo de Moura
|
fc4e304b27
|
refactor(library): move equations to equations_compiler
|
2016-08-11 10:08:30 -07:00 |
|