Leonardo de Moura
a823b0e6ec
feat(library/type_context): pop_local for type_context
2016-03-09 10:22:48 -08:00
Leonardo de Moura
c679c3a8d4
dev(kernel/abstract_type_context): extend abstract_type_context API
2016-03-08 11:40:36 -08:00
Leonardo de Moura
45cbb7c676
dev(library/type_context): add missing fields
2016-03-08 11:27:34 -08:00
Leonardo de Moura
99145073ef
chore(library/type_context): fix style
2016-03-08 10:16:11 -08:00
Leonardo de Moura
c36cf16a11
feat(library/type_context): new type_context skeleton
2016-03-05 21:53:27 -08:00
Leonardo de Moura
fcf3e2e065
fix(library/local_context): typo
2016-03-05 16:57:15 -08:00
Leonardo de Moura
c0fc9e5479
feat(library/local_context, library/metavar_context): add new well_formed methods and procedures
2016-03-05 14:56:13 -08:00
Leonardo de Moura
fdbe8ee98a
feat(library/local_context): add get_local_decl_from_user_name
2016-03-05 13:35:54 -08:00
Leonardo de Moura
c8e5907b70
feat(util/rb_tree,util/rb_map): add back_find_if
2016-03-05 13:29:34 -08:00
Leonardo de Moura
c3568e1ebb
fix(library/local_context): typo in assertion
2016-03-05 13:28:33 -08:00
Leonardo de Moura
66d583d279
feat(library/local_context): add well_formed debugging methods
2016-03-05 13:09:36 -08:00
Leonardo de Moura
4543dc4a7f
feat(library): add metavar_context
2016-03-05 12:53:45 -08:00
Leonardo de Moura
994c9298b5
feat(library/local_context): add local_decls (set), and freeze operation for local declarations
2016-03-04 13:59:11 -08:00
Leonardo de Moura
05f58547c5
chore(library/type_context): rename type_context to old_type_context
...
We are going to implement a new type_context object.
2016-03-04 10:51:04 -08:00
Leonardo de Moura
eaac6ba721
chore(library/type_context): rename default_type_context to legacy_type_context and move it to different file
2016-03-04 10:26:50 -08:00
Leonardo de Moura
e7f641ffc4
chore(library): cleanup proofs
2016-03-03 17:37:24 -08:00
Leonardo de Moura
9d0dfb8404
refactor(frontends/lean): remove calc_proof_elaborator
2016-03-03 17:22:45 -08:00
Leonardo de Moura
227b548341
refactor(frontends/lean/calc): no overloading in calc steps
2016-03-03 15:00:51 -08:00
Leonardo de Moura
2c70ca83a8
refactor(frontends/lean/calc): remove '{}' notation for eq.subst in calc mode
2016-03-03 14:18:20 -08:00
Leonardo de Moura
d7de521126
refactor(library/class): remove attribute [multiple_instances] and old type class resolution procedure
2016-03-03 13:58:22 -08:00
Leonardo de Moura
4a43e33d45
chore(*): disable big chunk of the standard library and tests
2016-03-03 13:43:08 -08:00
Leonardo de Moura
f0158ba20c
chore(CMakeLists): disable HoTT library and tests
2016-03-03 12:51:10 -08:00
Floris van Doorn
5cacebcf86
feat(hott): replace assert by have and merge namespace equiv.ops into equiv
...
The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ
2016-03-03 10:13:21 -08:00
Floris van Doorn
058000f61d
feat(homotopy/homotopy_group): add theorems in section 8.3 of the HoTT book
2016-03-03 10:13:21 -08:00
Floris van Doorn
1903601ba5
refactor(trunc): rename namespace is_trunc.trunc_index to trunc_index
2016-03-03 10:13:20 -08:00
Floris van Doorn
e2b31a9b33
feat(hott): remove multiple_instances attribute
2016-03-03 10:13:20 -08:00
Floris van Doorn
af4ba3d2fb
feat(hott): prove that the (n+1)-sphere is n-connected
2016-03-03 10:13:20 -08:00
Floris van Doorn
e515875464
feat(hott): various additions
2016-03-03 10:13:20 -08:00
Floris van Doorn
c6e628da12
feat(hott): more computation rules for trunc_index and use nats for Lemma 8.6.2
2016-03-03 10:13:20 -08:00
Floris van Doorn
e5d5ef9d55
feat(hott/library): various changes and additions.
...
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
2016-03-03 10:13:20 -08:00
Floris van Doorn
65b367ddff
feat(fin): port more parts of fin from the standard library
2016-03-03 10:13:20 -08:00
Floris van Doorn
bf403e124a
feat(nat/div): port to HoTT library
2016-03-03 10:13:20 -08:00
Floris van Doorn
4238fdd3d8
fix(hott): add missing links to markdown files
2016-03-03 10:13:20 -08:00
Leonardo de Moura
d84a20d68b
remove(frontends/lean/server): FINDG command
2016-03-03 10:12:24 -08:00
Leonardo de Moura
22f3efc5be
remove(frontends/lean): begin_end pre-tactics
...
This was never used
2016-03-03 10:02:09 -08:00
Leonardo de Moura
d54a67cf2e
fix(library): compilation warnings on OSX
2016-03-03 10:02:00 -08:00
Leonardo de Moura
6f766dd33e
chore(library/blast): cleanup
2016-03-03 10:01:50 -08:00
Jeremy Avigad
87252bbffe
fix(library/data/set/basic): add spaces in notation for bounded quantifiers
2016-03-03 11:50:40 -05:00
Jeremy Avigad
dc6cd71236
fix(library/algebra/monotone): fix theorem names
2016-03-02 22:54:51 -05:00
Jeremy Avigad
4050892889
refactor(library/*): rename 'compose' to 'comp'
2016-03-02 22:48:05 -05:00
Jeremy Avigad
ebb3e60096
feat(library/algebra/monotone): add properties of monotone functions
2016-03-02 22:01:35 -05:00
Jeremy Avigad
3d09144d73
feat(library/algebra/homomorphism): add homomorphisms between algebraic structures
2016-03-02 19:45:45 -05:00
Leonardo de Moura
5194df5e97
feat(library/local_context): encode order using a tree instead of a list
...
Motivations:
- It will be faster to delete local declarations.
- It is faster to find all local declarations that were created after a
give local declaration.
2016-03-01 16:23:51 -08:00
Leonardo de Moura
82fb38b440
feat(util/rb_tree): add for_each_greater
2016-03-01 15:42:27 -08:00
Leonardo de Moura
2a4b3b75bd
refactor(library/blast/state): simplify blast state
2016-03-01 14:27:58 -08:00
Leonardo de Moura
16dc021736
fix(library/proof_irrel_expr_manager): add missing Let case
2016-03-01 14:27:37 -08:00
Jakob von Raumer
1104537d02
chore(hott) adjust to new naming for pointed types and truncated types
2016-03-01 13:52:53 -08:00
Jakob von Raumer
2b13777bbe
feat(hott) add type functors, maybe they should be changed to be un-funexted.
2016-03-01 13:52:53 -08:00
Jakob von Raumer
11458f64fe
feat(hott/algebra) add order categories
2016-03-01 13:52:53 -08:00
Leonardo de Moura
4e67a35179
feat(library/blast/blast): add missing Let case, and comment to indicate
...
performance problem
2016-03-01 13:47:43 -08:00
