lean4-htt/library
Leonardo de Moura e9b4b811de chore(library/equations_compiler/util): disable generation of equational lemmas
@kha, `eqn_compiler.lemmas` is false by default.
I will keep them disabled until I remove the inductive compiler.
I'm building the new inductive datatype module (to replace the inductive
compiler), and the lemmas will fail to be proved in the next commits
until the transition is complete.
2018-06-12 13:03:25 -07:00
..
init chore(library/equations_compiler/util): disable generation of equational lemmas 2018-06-12 13:03:25 -07:00
system chore(*): remove more files 2018-05-21 06:42:58 -07:00
leanpkg.path feat(leanpkg): add package manager 2017-05-01 14:11:38 -07:00
library.md chore(library/library.md): update documentation 2017-08-16 14:17:26 -07:00