Leonardo de Moura
bedb508a8f
feat(library/equations_compiler): do not generate bytecode for lemmas
2016-09-06 15:14:47 -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
01107f7aae
feat(library/equations_compiler): generate bytecode for auxiliary definitions
2016-09-06 13:29:12 -07:00
Leonardo de Moura
d8caecff49
refactor(library/exception): avoid throw_generic_exception functions
2016-09-06 12:37:56 -07:00
Leonardo de Moura
cfbffb41ef
feat(library/equations_compiler): prove equation lemmas that use if-then-else
2016-09-03 13:23:09 -07:00
Leonardo de Moura
13f0d4e09a
refactor(library/equations_compiler): new equation lemma generation
...
The idea is to generate a lemma based on the left-hand-side provided by
the user. This feature is essential for supporting the derived inductive
datatype constructors.
2016-09-02 14:04:09 -07:00
Leonardo de Moura
bf096eb292
chore(library/equations_compiler/structural_rec): "lemmas" ==> "equations"
2016-09-02 11:17:38 -07:00
Leonardo de Moura
54fd9adb47
feat(library/equations_compiler): use defeq simplifier to cleanup types of automatically synthesized lemmas
2016-08-31 15:54:03 -07:00
Leonardo de Moura
51a338d9a1
fix(library/equations_compiler/structural_rec): support for reflexive inductive datatypes
2016-08-31 10:46:32 -07:00
Leonardo de Moura
924c98832b
feat(library/equations_compiler/structural_rec): generate eqn lemmas at structural_rec
2016-08-31 09:07:17 -07:00
Leonardo de Moura
33514dd6ea
feat(library/equations_compiler/structural_rec): process aux lemmas
2016-08-30 20:09:57 -07:00
Leonardo de Moura
2fc0e5fa05
feat(library/equations_compiler/structural_rec): add aux definition
2016-08-30 18:33:24 -07:00
Leonardo de Moura
230db1bc92
feat(library/equations_compiler/structural_rec): generate brec_on-based function
...
We still need to generate lemmas and induction principle.
2016-08-29 15:58:13 -07:00
Leonardo de Moura
f1f45cc2b7
feat(library/equations_compiler/structural_rec): better support for structural recursion (based on brec_on)
...
For example, before this commit, structural_rec would not support the
function to_nat defined below.
```
set_option new_elaborator true
inductive foo : bool → Type
| Z : foo ff
| O : foo ff → foo tt
| E : foo tt → foo ff
definition to_nat : ∀ {b}, foo b → nat
| .ff Z := 0
| .tt (O n) := to_nat n + 1
| .ff (E n) := to_nat n + 1
```
2016-08-29 10:51:09 -07:00
Leonardo de Moura
b08af16d5f
refactor(library/equations_compiler): remove unnecessary abstraction
...
We changed how we are going to process derived inductive datatypes.
2016-08-29 09:25:01 -07:00
Leonardo de Moura
7669e18c77
feat(library/equations_compiler): add unbounded_rec
2016-08-16 12:54:54 -07:00
Leonardo de Moura
532a38befa
feat(library/equations_compiler/structural_rec): finish structural recursion step
2016-08-16 08:08:51 -07:00
Leonardo de Moura
8b67480cee
feat(library/equations_compiler): add step for handling structural recursion
2016-08-15 18:00:25 -07:00
