Leonardo de Moura
e3e9220ab9
fix(library/tactic/rewrite_tactic): fixes #708
2015-06-26 18:41:08 -07:00
Leonardo de Moura
c61e6f6595
feat(library/unifier): add new rule for constraints of the form (pr ...) =?= t, where (pr ...) is a "stuck" projection application
2015-06-26 17:18:29 -07:00
Leonardo de Moura
0b7859f387
feat(library,frontends/lean): add support for projections in the elaborator
...
The idea is to simulate the computation rules such as
pr1 (mk a b) ==> a
in the elaborator
2015-06-26 17:18:29 -07:00
Leonardo de Moura
31a4ee2ac3
fix(library/inductive_unifier_plugin): avoid potential assertion violation
2015-06-26 17:18:29 -07:00
Leonardo de Moura
a680114fd8
fix(library/tactic/rewrite_tactic): potential crash in the rewrite tactic
2015-06-26 17:18:29 -07:00
Floris van Doorn
c8eee66c5b
feat(hott/relation): add equivalence closure of a relation
2015-06-25 22:31:41 -04:00
Floris van Doorn
ea0f57aef5
feat(hott): various clean-up and small additions
2015-06-25 22:31:40 -04:00
Leonardo de Moura
5581b735f4
feat(library/constants.txt): add poly_unit and poly_unit.star
2015-06-25 17:36:34 -07:00
Floris van Doorn
fa1979c128
feat(datatypes): let the type of unit be the lowest non-Prop universe
...
The definitional package (brec_on and cases_on) now use poly_unit instead of unit
closes #698
2015-06-25 17:33:46 -07:00
Leonardo de Moura
919c4ea8ee
feat(frontends/lean/calc_proof_elaborator): cleanup communication between unifier and calc_proof_elaborator
2015-06-24 14:14:44 -07:00
Leonardo de Moura
a2389fb664
refactor(kernel/default_converter): move delay_check code to postpone_is_def_eq method
2015-06-22 13:59:32 -07:00
Leonardo de Moura
76477aedd1
refactor(kernel): move is_stuck predicate to converter
2015-06-22 11:37:14 -07:00
Leonardo de Moura
5687c24944
refactor(library/tactic/induction_tactic): cleanup
2015-06-22 10:23:54 -07:00
Leonardo de Moura
54496709a2
refactor(kernel/default_converter): add virtual method reduce_def_eq
...
The idea is to allow us to customize the default converter outside of
the kernel.
2015-06-22 10:04:19 -07:00
Leonardo de Moura
a518a45239
refactor(kernel/default_converter): separate lazy_delta_reduction procedure
2015-06-22 08:45:05 -07:00
Leonardo de Moura
1c70514231
feat(frontends/lean/structure_cmd): disable conversion optimization for automatically generated coercions
2015-06-21 16:57:37 -07:00
Leonardo de Moura
aeea8f83c4
feat(library/composition_manager): check if existing definition is definitionally equal
2015-06-21 16:53:08 -07:00
Leonardo de Moura
e3062c64e2
feat(util/timeit): avoid scientific notation when displaying runtimes
2015-06-21 14:52:27 -07:00
Leonardo de Moura
b8243934de
feat(library/tc_multigraph): finish transitive closed multigraph
2015-06-20 20:25:20 -07:00
Leonardo de Moura
3626bd83bf
refactor(util/sexpr/format): remove format constructors using std::initializer_list
...
For some reason lean.js (Lean compiled using emscripten) crashes when
this kind of constructor is used.
2015-06-20 14:02:18 -07:00
Leonardo de Moura
d28c26b6eb
feat(util/sexpr/format): small change
...
The idea is to avoid unnecessary memory allocations.
It may also help with the lean.js problem we are fighting with.
2015-06-19 21:21:28 -07:00
Leonardo de Moura
c6ad37a651
chore(src/library/tc_multigraph): fix typo
2015-06-19 21:12:11 -07:00
Leonardo de Moura
38394d85dd
fix(util/sexpr/format): potential access memory violation
2015-06-19 20:26:35 -07:00
Leonardo de Moura
accc9dc38b
chore(util/sexpr/format): remove unnecessary method
2015-06-19 20:11:42 -07:00
Leonardo de Moura
6872761c67
fix(library/tc_multigraph): typos
2015-06-19 20:11:31 -07:00
Leonardo de Moura
1f753aeccb
feat(library): add tc_multigraph skeleton
2015-06-19 20:05:05 -07:00
Leonardo de Moura
70fc05294b
refactor(library/local_context): avoid hack in local_context
2015-06-18 15:41:00 -07:00
Leonardo de Moura
694eef7f6a
fix(util/sexpr/format): retract change that may be creating problems for emscripten
2015-06-18 10:49:13 -07:00
Leonardo de Moura
42c236eb2e
chore(shell/emscripten): fix style
2015-06-18 10:23:49 -07:00
Leonardo de Moura
a24b06254b
test(tests/shell): add unit test for emscripten_shell
2015-06-18 10:20:26 -07:00
Leonardo de Moura
a6fe4cbce6
refactor(shell): move emscripten_shell to a separate file
2015-06-18 09:53:23 -07:00
Leonardo de Moura
a4c0699e81
feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic
...
See issue #676
Add new test demonstrating why it is useful to have the old semantics
for 'constructor'
2015-06-17 23:48:54 -07:00
Leonardo de Moura
bf71d9f342
fix(library/tactic/rewrite_tactic): fixes #682
2015-06-17 18:49:02 -07:00
Leonardo de Moura
2109dff46a
feat(frontends/lean): remove unnecessary flag
2015-06-17 17:23:20 -07:00
Leonardo de Moura
ce8f2a1674
feat(library/class): allow any constant to be marked as a class
...
closes #679
2015-06-17 16:26:45 -07:00
Leonardo de Moura
9e6e406f73
feat(frontends/lean): add '#compose' command for testing composition manager
2015-06-17 14:42:25 -07:00
Leonardo de Moura
c59e1f49db
feat(library): add composition manager
2015-06-17 14:41:50 -07:00
Leonardo de Moura
14c33c4e01
feat(kernel/error_msgs): add workaround for issue #669
...
This issue should fix the new problem reported at #669 .
It only disables beta-reduction in the pretty printer for application
type mismatch at (f n) when f is a lambda expression.
2015-06-17 12:00:25 -07:00
Leonardo de Moura
f60cdee14b
fix(library/tactic/rewrite_tactic): memory leak
2015-06-16 15:47:21 -07:00
Leonardo de Moura
0ae24faae3
feat(library/tactic/constructor_tactic): use 'fapply' in 'constructor' tactic
...
closes #676
2015-06-16 12:03:31 -07:00
Leonardo de Moura
2277b170f6
feat(library/tactic/exact_tactic): use 'append' instead of 'orelse' at eassumption 'tactic'
2015-06-16 11:58:10 -07:00
Leonardo de Moura
169f956143
fix(library/tactic): remove dead code
2015-06-16 11:57:37 -07:00
Leonardo de Moura
d8620ef4c9
fix(kernel,library,frontends/lean): improve error messages
...
see #669
2015-06-14 19:44:00 -07:00
Leonardo de Moura
8699d2dfb7
feat(library/tactic/rewrite_tactic): display list of overloads occurring in a failed rewrite step
2015-06-14 16:30:18 -07:00
Leonardo de Moura
382d4d32b7
feat(frontends/lean): 'override' command and '#<namespace> <expr>' notation also override aliases
...
Before this commit they were only overriding notation declarations.
2015-06-14 15:48:36 -07:00
Leonardo de Moura
01f8f3c11d
fix(frontends/lean): memory access violation
2015-06-14 15:37:45 -07:00
Leonardo de Moura
45684588cc
fix(frontends/lean/nested_declaration): compilation error in debug mode
2015-06-13 13:10:10 -07:00
Leonardo de Moura
8a85e4ee87
feat(frontends/lean/builtin_cmds): improve print <id> when <id> is a not yet revealed theorem
...
We add a remark saying the command `reveal <id>` should be used to
access `<id>` definition.
2015-06-13 12:12:22 -07:00
Leonardo de Moura
591fb91f34
fix(frontends/lean/builtin_cmds): fixes #671
2015-06-13 11:35:03 -07:00
Leonardo de Moura
9fbf267a3f
feat(library/tactic/rewrite_tactic): when 'rewrite' step fails apply esimp and try again
...
closes #670
2015-06-12 19:48:58 -07:00
