Leonardo de Moura
760dc2162a
chore(library/definitional/equations): cleanup
2015-01-06 14:53:21 -08:00
Leonardo de Moura
a3a6697f44
feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes
2015-01-06 14:07:17 -08:00
Leonardo de Moura
c33928f202
fix(library/pp_options): memory leak
2015-01-06 10:22:23 -08:00
Leonardo de Moura
322cdb8a98
feat(library/definitional/equations): add 'equations_result' macro used to wrap multiple functions being defined by recursive equations
...
This is only useful when compiling "mutually recursive" functions.
2015-01-05 19:09:20 -08:00
Leonardo de Moura
3325d791de
fix(library/definitional/equations): bug in recursive application elimination
2015-01-05 17:17:14 -08:00
Leonardo de Moura
eedc31f7e9
fix(library/definitional/equations): bug in "complete" transition
2015-01-05 16:27:29 -08:00
Leonardo de Moura
3889b60152
feat(library/definitional/equations): allow inductive datatype parameters in recursive equations
2015-01-05 15:56:28 -08:00
Leonardo de Moura
6eba4b4ac1
chore(library/definitional/equations): cleanup
2015-01-05 13:57:13 -08:00
Leonardo de Moura
b46c377aa2
feat(library/definitional/equations): add "complete" transition for overlapping patterns
2015-01-05 11:49:27 -08:00
Leonardo de Moura
fdef3e5407
feat(library/definitional/equations): add support for reflexive datatypes in the definitional package
2015-01-05 11:13:35 -08:00
Leonardo de Moura
5e228d92d2
fix(library/definitional/equations): missing case
2015-01-04 20:49:53 -08:00
Leonardo de Moura
576c053c25
fix(library/tactic/inversion_tactic): bug at implementation_list update
2015-01-04 19:56:10 -08:00
Leonardo de Moura
faf78ce3e6
feat(library/definitional/equations): brec_on compilation
2015-01-04 17:45:13 -08:00
Leonardo de Moura
98a856373d
feat(library/util): add dec_level auxiliary procedure
2015-01-04 13:25:58 -08:00
Leonardo de Moura
926c140e17
fix(library/definitional/equations): fix clang compilation problems
2015-01-04 10:18:19 -08:00
Leonardo de Moura
bdfa919098
feat(library/definitional/equations): add brec_on based compilation
2015-01-03 22:23:37 -08:00
Leonardo de Moura
42354cd4fa
feat(library/locals): add auxiliary templates
2015-01-03 22:23:08 -08:00
Leonardo de Moura
376126241e
fix(library/definitional/equations): typo and bug
2015-01-03 15:29:34 -08:00
Leonardo de Moura
21a9cd58a3
fix(library/definitional/equations): bug when compiling in proof relevant kernels
2015-01-02 23:17:33 -08:00
Leonardo de Moura
7f7d318b22
feat(library/definitional/equations): add dependent pattern matching compilation
2015-01-02 22:06:40 -08:00
Leonardo de Moura
762a515a5b
feat(library/tactic/inversion_tactic): mark new arguments that have been "unified" into terms
2015-01-02 22:02:15 -08:00
Leonardo de Moura
3fb2d8bbc0
feat(library/tactic/inversion_tactic): use the "simpler" compilation approach in more cases
...
The approach implemented in the commit 8974d70c11ef7b9b2c5d can be
extended to indexed inductive families. See comments in the code.
2015-01-01 19:33:15 -08:00
Leonardo de Moura
be9e2500ce
feat(library/tactic/inversion_tactic): add more efficient "compilation" for non-indexed inductive datatypes
2015-01-01 19:33:14 -08:00
Leonardo de Moura
57490a6431
feat(library/tactic/inversion_tactic): avoid unnecessary eq.rec's
2015-01-01 19:33:14 -08:00
Leonardo de Moura
58f052b1bb
fix(library/normalize): unitialized variable
2015-01-01 19:33:14 -08:00
Leonardo de Moura
761810f350
feat(library/tactic/inversion_tactic): generate auxiliary information
2015-01-01 19:33:14 -08:00
Leonardo de Moura
1f13bfa4f7
feat(library/tactic/inversion_tactic): add inversion::apply procedure
...
The new procedure is essentially a "customized" version of the
inversion (aka cases) tactic for the equations package
2015-01-01 19:33:14 -08:00
Leonardo de Moura
1d79cb9c07
fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library
2014-12-22 09:40:15 -08:00
Leonardo de Moura
d2958044fd
feat(frontends/lean): add multiple_instances command
...
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command
multiple_instances <class-name>
closes #370
2014-12-21 17:28:44 -08:00
Leonardo de Moura
5efadb09cc
feat(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT library
...
This commit adds support for hypotheses (h : C As idxs) where the indices idxs
are just local constants. Before this commit the indices idxs had to be hsets.
Now, they can be hsets or local constants.
The new tests demonstrate new examples that can be handled by the
improved tactic in the HoTT library
2014-12-21 15:19:25 -08:00
Leonardo de Moura
677ec2a2fe
feat(library/tactic/inversion_tactic): adjust inversion tactic to HoTT lib
2014-12-20 11:32:27 -08:00
Leonardo de Moura
2070ac849c
feat(library/util): add get_intro_rule_names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-20 11:31:48 -08:00
Leonardo de Moura
d9d822baa7
feat(library/tactic/class_instance_synth): add mk_hset_instance procedure
2014-12-19 22:00:25 -08:00
Leonardo de Moura
8c63045492
feat(library/util): add more auxiliary procedures
2014-12-19 22:00:25 -08:00
Leonardo de Moura
d6f79423e9
feat(library/tactic/class_instance_synth): add mk_class_instance procedures
2014-12-19 20:09:09 -08:00
Leonardo de Moura
4421069e34
refactor(library/tactic): rename placeholder_elaborator to class_instance_synth
2014-12-19 19:57:38 -08:00
Leonardo de Moura
ded869b7e0
refactor(frontends/lean): move placeholder_elaborator to library/tactic
2014-12-19 15:23:22 -08:00
Leonardo de Moura
a22dc773b7
refactor(frontends/lean): move some auxiliary procedures to library/tactic
2014-12-19 15:19:45 -08:00
Leonardo de Moura
69750c50c6
refactor(frontends/lean): move pp_options to library
2014-12-19 15:00:05 -08:00
Leonardo de Moura
caf0a4bf15
refactor(frontends/lean): move type_checker_ptr typedef to library
2014-12-19 14:40:15 -08:00
Leonardo de Moura
02de288a51
refactor(frontends/lean): move choice_iterator to library
2014-12-19 14:29:32 -08:00
Leonardo de Moura
9bd74689be
feat(library/util): add mk_refl
2014-12-19 13:54:12 -08:00
Leonardo de Moura
a97bef7df2
feat(library/util): add mk_heq
2014-12-19 13:54:12 -08:00
Leonardo de Moura
1ca8723c54
refactor(library/util): allow mk_telescopic_eq to be used with (terms, locals)
2014-12-19 13:54:12 -08:00
Leonardo de Moura
6f78315aa4
refactor(*): add uniform names for "meta-objects"
2014-12-17 11:42:14 -08:00
Leonardo de Moura
8939351903
refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception
2014-12-15 19:22:17 -08:00
Leonardo de Moura
5a9cd9eed4
fix(library/normalize): bug in the "eval" command
2014-12-15 19:22:17 -08:00
Leonardo de Moura
f0b002d5a7
fix(library/aliases): aliases in sections and contexts
2014-12-13 14:57:15 -08:00
Leonardo de Moura
e897bbdeb9
feat(library/util): add auxiliary functions for creating tuples (using sigma types)
2014-12-11 17:31:47 -08:00
Leonardo de Moura
b8f665e561
feat(frontends/lean): elaborate recursive equations
...
Remark: we are not compiling them yet.
2014-12-10 22:25:40 -08:00
