Leonardo de Moura
aa0abd5cef
fix(library/equations_compiler/structural_rec): bug in decoder
2016-12-18 22:51:02 -08:00
Leonardo de Moura
b75e8b99f5
fix(library/equations_compiler/structural_rec): missing case: reflexive inductive type eliminating into Prop
...
see #1199
2016-11-23 13:56:01 -08:00
Leonardo de Moura
823357462e
feat(library/equations_compiler/structural_rec): validation
2016-09-23 13:50:55 -07:00
Leonardo de Moura
c8e13cd391
feat(frontends/lean): minimize errors being reported
2016-09-23 09:20:31 -07:00
Leonardo de Moura
5e5285ee67
refactor(library): rename pr1/pr2 ==> fst/snd
2016-09-21 09:48:39 -07:00
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
9d9f2b2636
fix(library/equations_compiler/structural_rec): bug at check_arg_type
2016-09-18 18:36:20 -07:00
Leonardo de Moura
194d1be0dd
fix(library/equations_compiler/structural_rec): reflexive type support
2016-09-18 16:15:31 -07:00
Leonardo de Moura
7fb407d2fd
fix(library/equations_compiler/structural_rec): typo
2016-09-16 07:56:28 -07:00
Leonardo de Moura
e6dd5242fc
feat(library/equations_compiler): add option eqn_compiler.zeta
2016-09-10 14:00:16 -07:00
Leonardo de Moura
50ef0185d9
fix(library/equations_compiler/structural_rec): missing relaxed_whnf
2016-09-10 12:14:00 -07:00
Leonardo de Moura
96fa8856bc
feat(library/equations_compiler): add mk_nonrec
2016-09-08 14:09:05 -07:00
Leonardo de Moura
14d009ce92
refactor(library/equations_compiler): improve mk_equation_lemma
2016-09-08 11:50:58 -07:00
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
