Leonardo de Moura
a1e8610e64
fix(library/type_context): take annotations into account at is_stuck
2016-08-30 08:29:15 -07:00
Leonardo de Moura
85cf20a5b4
fix(library/type_context): missing case: stuck projections
...
type_context only unfolds projections when they reduce.
2016-08-30 08:13:58 -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
78f81034c6
feat(library): add helper methods
2016-08-29 08:31:33 -07:00
Leonardo de Moura
b317d4bc58
refactor(library/tactic): add hsubstitution module
2016-08-29 08:19:05 -07:00
Leonardo de Moura
cb7c82fdd5
feat(library/type_context): make sure annotations are ignored at is_def_eq
2016-08-28 14:42:50 -07:00
Leonardo de Moura
1a675d69fc
refactor(library/tactic/induction_tactic,library/tactic/cases_tactic): replace name_map<name> with substitutions at induction_tactic
...
This commit also removes dead code from cases_tactic
2016-08-28 14:09:22 -07:00
Leonardo de Moura
206bf613d5
feat(library/tactic/subst_tactic): use substitutions instead of name_map<name> in the subst_tactic (low level) API
2016-08-28 13:29:44 -07:00
Leonardo de Moura
f0f9880ece
refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic):
...
new design for elim_match
I still need to fix lemma generation, and refactor induction/subst tactics
2016-08-28 13:15:10 -07:00
Leonardo de Moura
af7060b46e
chore(library/tactic/cases_tactic): add trace
2016-08-28 07:57:20 -07:00
Leonardo de Moura
19a6005f7e
refactor(library): move user_attribute to tactic folder
...
It depends on tactic_state.
2016-08-26 09:28:42 -07:00
Leonardo de Moura
95e8228e8a
refactor(library/tactic/cases_tactic): improve low-level API
2016-08-25 16:34:40 -07:00
Leonardo de Moura
98aefca014
fix(library/local_context): depends_on should take into account assigned metavariables
2016-08-25 13:49:54 -07:00
Leonardo de Moura
c032505023
chore(library/tactic/subst_tactic): missing '\n' in trace msg
2016-08-25 13:45:04 -07:00
Leonardo de Moura
20ae4200e4
feat(library/tactic/tactic_state): add option for instantiating mvars before printing goal (default is true)
2016-08-25 11:11:52 -07:00
Leonardo de Moura
cf15218eea
chore(library/equations_compiler/compiler): add new trace option
2016-08-25 10:45:08 -07:00
Leonardo de Moura
41b6358de6
chore(library/equations_compiler/elim_match): add helper methods
2016-08-25 10:44:50 -07:00
Sebastian Ullrich
441a219a66
feat(library/attribute_manager): make attributes with side-effect free callbacks removable
2016-08-23 21:52:52 -07:00
Leonardo de Moura
f86ed747cc
feat(library/type_context): use default cache_manager when one is not provided, add trace msgs for caching
2016-08-23 21:31:10 -07:00
Leonardo de Moura
7851b9c097
fix(frontends/lean/definition_cmds): parameter handling
2016-08-23 21:13:54 -07:00
Leonardo de Moura
55bd3e223e
feat(library/type_context): add set_env
2016-08-23 18:32:58 -07:00
Leonardo de Moura
a93eada058
feat(library/type_context): improved (and simplified) cache management for type_context
2016-08-23 17:56:58 -07:00
Leonardo de Moura
5dca96a2a2
feat(library/attribute_manager): add get_attribute_fingerprint C++ API
2016-08-23 15:41:40 -07:00
Leonardo de Moura
bc3b01828d
fix(library/attribute_manager): memory leak
...
The method `release` releases the pointer ownership without deleting it.
2016-08-23 15:40:51 -07:00
Leonardo de Moura
871d78fbf8
fix(library/tactic/simplifier/simplifier): memory leaks at simplifier
2016-08-23 15:34:58 -07:00
Sebastian Ullrich
abd040589f
feat(frontends/lean/decl_attributes, library/attribute_manager): implement attribute removal
2016-08-23 14:09:35 -07:00
Sebastian Ullrich
a4f338889d
chore(library/attribute_manager): remove dead code
2016-08-23 14:09:35 -07:00
Sebastian Ullrich
6e2f7c107c
refactor(library/attribute_manager): rename on_set and move up into attribute base class
2016-08-23 14:09:35 -07:00
Leonardo de Moura
e4fd627ae2
feat(library/attribute_manager): fingerprints
...
The fingerprint changes whenever a new attribute is added.
2016-08-23 08:20:37 -07:00
Leonardo de Moura
9979bf7cea
chore(library): formatting
2016-08-23 07:56:01 -07:00
Leonardo de Moura
199decea51
fix(library/tactic/tactic_state): remove problematic get_tactic_vm_state
2016-08-23 07:38:44 -07:00
Leonardo de Moura
27e06c80ba
feat(library/equations_compiler/elim_match): generate auxiliary definition and lemmas for match
2016-08-22 17:59:54 -07:00
Leonardo de Moura
3de9509644
feat(library/aux_definition): add helper functions for creating auxiliary definitions
2016-08-22 17:59:40 -07:00
Leonardo de Moura
d8447b4c53
feat(library/equations_compiler/elim_match): add noequation transition
2016-08-22 13:53:35 -07:00
Leonardo de Moura
714817edd5
fix(library/equations_compiler/util): missing get_constructors_of
2016-08-22 13:42:34 -07:00
Leonardo de Moura
963503838c
fix(library/equations_compiler/util): support for noequation
2016-08-22 13:42:03 -07:00
Leonardo de Moura
9ad64e9176
feat(library/equations_compiler/elim_match): complete transition
2016-08-22 13:23:51 -07:00
Leonardo de Moura
2587164999
fix(library/user_recursors): missing statement
2016-08-22 09:38:43 -07:00
Leonardo de Moura
bd35bb4bdd
fix(library/user_recursors): g++ false warning
2016-08-22 09:30:22 -07:00
Leonardo de Moura
8e63769413
chore(library/tactic/subst_tactic): remove 'static' to avoid warning in release mode
2016-08-22 09:23:18 -07:00
Leonardo de Moura
440d30300f
fix(library/tactic/simplifier/simp_lemmas): typo
2016-08-21 22:30:16 -07:00
Leonardo de Moura
e81d92006b
feat(library/equations_compiler/elim_match): try to use user-provided names in the variable transition
2016-08-21 22:20:31 -07:00
Leonardo de Moura
038a250798
feat(library/equations_compiler/elim_match): add skip transition for inaccessible terms
2016-08-21 22:11:28 -07:00
Leonardo de Moura
9c55ede671
fix(library/equations_compiler/elim_match): constructor transition
2016-08-21 21:49:45 -07:00
Leonardo de Moura
a4577901e8
fix(library/user_recursors): add support for automatically generated recursors
2016-08-21 17:17:48 -07:00
Leonardo de Moura
67dc68b24d
feat(library/equations_compiler/elim_match): add variable/constructor transitions
2016-08-21 15:56:32 -07:00
Leonardo de Moura
2d90c73546
chore(library/equations_compiler/util): add helper method
2016-08-21 15:55:56 -07:00
Leonardo de Moura
1ea3bc1683
fix(library/tactic/cases_tactic): lowlevel interface that gives access to renamed/introduced hypotheses
2016-08-21 15:55:56 -07:00
