Commit graph

6376 commits

Author SHA1 Message Date
Leonardo de Moura
bd28396be0 feat(kernel): transparent theorems
closes #576
2015-05-09 11:42:29 -07:00
Leonardo de Moura
f63c2d9393 feat(kernel/inductive/inductive): for datatypes that support K, we should try K before normalizing the major premise 2015-05-09 11:23:10 -07:00
Leonardo de Moura
8086ad7461 feat(library/init): define quot.hrec_on and quot.hrec_on₂ based on heterogeneous equality
They are easier to use than the version with nested eq.rec's
2015-05-09 09:49:41 -07:00
Leonardo de Moura
d217655a62 fix(kernel/quotient/quotient): bug in reduction rule for quot.ind 2015-05-09 09:07:03 -07:00
Leonardo de Moura
4e35afedcc feat(frontends/lean): rename 'wait' to 'reveal'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-05-08 20:54:16 -07:00
Leonardo de Moura
f8e2f68ce0 feat(frontends/lean): add 'wait' command
This commit also fixes several problems with -j option (parallel
compilation). The .olean files were not missing data when -j was used

see issue #576
2015-05-08 20:05:21 -07:00
Leonardo de Moura
e6566e5814 fix(frontends/lean/parser): incorrect error message 2015-05-08 18:13:44 -07:00
Leonardo de Moura
e59456c19f feat(frontends/lean): remove 'opaque' keyword
see issue #576
2015-05-08 16:45:13 -07:00
Leonardo de Moura
4f0f739ea6 feat(library): remove occurrences of 'opaque' keyword 2015-05-08 16:40:03 -07:00
Leonardo de Moura
cf7e60e5a6 refactor(kernel): remove "opaque" field from kernel declarations
see issue #576
2015-05-08 16:06:16 -07:00
Leonardo de Moura
6c958a25e7 refactor(library/tactic/expr_to_tactic): make sure builtin tactics don't need to be marked opaque
This modification is needed since we will remove opaque definitions from
the kernel.

see issue #576
2015-05-08 16:06:16 -07:00
Leonardo de Moura
57ea660963 refactor(*): start process for eliminating of opaque definitions from the kernel
see issue #576
2015-05-08 16:06:04 -07:00
Leonardo de Moura
061e26157e fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
Leonardo de Moura
72663e8a06 feat(library/tactic/rewrite_tactic): take hypotheses into account when checking rewrite step 2015-05-08 11:34:50 -07:00
Leonardo de Moura
746e6dc0ff fix(tests/lean): adjust tests output to reflect recent changes in the pretty printer 2015-05-08 11:11:00 -07:00
Leonardo de Moura
3aac370629 fix(library/data/finset/basic): type error on the finset.induction proof 2015-05-08 11:08:24 -07:00
Leonardo de Moura
12bad8794b feat(frontends/lean/pp): use 'assert' instead of 'have ... [visible]' 2015-05-08 10:02:15 -07:00
Jeremy Avigad
624b664950 refactor(library/data/list/basic.lean): make minor renaming 2015-05-08 20:25:28 +10:00
Jeremy Avigad
75e50fd371 feat(library/data): update defaults and markdown files 2015-05-08 20:23:15 +10:00
Jeremy Avigad
b56f7a06d5 refactor(library/data/finset/bigop.lean): use inter eq empty rather than disjoint 2015-05-08 20:06:21 +10:00
Jeremy Avigad
9beb70b292 feat(src/emacs/lean-input.el): add 'empty' as abbreviation for emptyset 2015-05-08 20:04:55 +10:00
Jeremy Avigad
6fce01385c feat(library/data/{finset,list}/bigop.lean: generalize bigops from group to monoid 2015-05-08 19:51:37 +10:00
Jeremy Avigad
42f2fc973a refactor(library/data/{finset,list,fintype}: rename cross_product to product 2015-05-08 19:51:37 +10:00
Jeremy Avigad
68f7afa053 feat(library/data/finset/card.lean): begin theory of cardinality 2015-05-08 19:51:37 +10:00
Jeremy Avigad
9e04d09381 feat(library/data/finset/comb.lean): add filter, diff, theorems 2015-05-08 19:51:37 +10:00
Jeremy Avigad
4db4c86d37 feat(library/data/finset/basic.lean): add lots of theorems, do minor renaming 2015-05-08 19:51:37 +10:00
Jeremy Avigad
a54a98c1ec feat(library/data/set): add distributivity, diff, uniformize with finset 2015-05-08 19:51:37 +10:00
Jeremy Avigad
9e26dddaf3 feat(library/data/list/perm): add perm_filter 2015-05-08 19:51:37 +10:00
Jeremy Avigad
86a039b6d5 feat(library/data/list/set.lean): add two theorems 2015-05-08 19:51:37 +10:00
Jeremy Avigad
e4c75ae8ae feat(library/logic/connective.lean): add distributivity laws 2015-05-08 19:51:37 +10:00
Jeremy Avigad
ba78cc42f9 fix(library/data/set/basic.lean, function.lean): fix typos 2015-05-08 19:51:37 +10:00
Leonardo de Moura
0b57f7d00a refactor(library/tactic): refine interface between tactic and proof-term modes
Some constraints were being lost with the previous interface.
This is why we had a workaround in fintype.lean.

We can also remove some hacks we have used in the past.
2015-05-07 18:02:51 -07:00
Leonardo de Moura
12b818b7d3 fix(library/util): "empty" is not universe polymorphic anymore 2015-05-07 16:43:58 -07:00
Floris van Doorn
ae43b244ef fix(tests): fix tests to reflect recent changes 2015-05-07 16:39:04 -07:00
Floris van Doorn
4c9eb2e3f4 chore(scripts): update documentation of port.pl, port.sh and rename.pl 2015-05-07 16:39:04 -07:00
Floris van Doorn
c2c7c4f79f feat(hit.circle): finish proof that (base = base) is equivalent to int 2015-05-07 16:39:04 -07:00
Floris van Doorn
111c8e1529 feat(hott): add [unfold-c] and [constructor] attributes for HITs 2015-05-07 16:39:04 -07:00
Floris van Doorn
9893de6194 feat(hit/circle): prove partly that the fundamental group of the circle is int
Also add markdown files for nat and int
2015-05-07 16:39:04 -07:00
Floris van Doorn
0a8f4f6dab feat(function): add unfold hints to function.[h]lean 2015-05-07 16:39:03 -07:00
Floris van Doorn
20e62c9623 fix(lean-syntax): add all metaclasses and the state tactic to syntax 2015-05-07 16:39:03 -07:00
Floris van Doorn
7cfac38eda feat(hott): port parts of natural numbers and integers from standard library to HoTT
This also involves:
- adding definitions about logic and natural numbers existing in the standard library to init
- porting the current algebraic hierarchy
2015-05-07 16:39:03 -07:00
Floris van Doorn
e9ff925e2f feat(pi): prove that forall x, a = x is a mere proposition 2015-05-07 16:39:03 -07:00
Floris van Doorn
e5241f84ec fix(init.datatypes): make empty live in Type.{0} 2015-05-07 16:39:03 -07:00
Floris van Doorn
90f1a691fd feat(hott): change notation of transport to correspond with standard library 2015-05-07 16:39:03 -07:00
Floris van Doorn
8b4756f9c8 feat(hott): port nat from standard library to HoTT library; make script to port files 2015-05-07 16:39:03 -07:00
Floris van Doorn
61c1cd6840 feat(hott.init): define core namespace 2015-05-07 16:39:03 -07:00
Floris van Doorn
6dfd7af0ec feat(hott.types): add theorems about booleans 2015-05-07 16:39:03 -07:00
Floris van Doorn
dce672a815 fix(hott.md): mention arity.hlean 2015-05-07 16:39:03 -07:00
Floris van Doorn
ce5f60d009 feat(hott.init.function): add more notions from the standard library 2015-05-07 16:39:03 -07:00
Floris van Doorn
43fb334914 feat(circle): prove loop != base 2015-05-07 16:39:03 -07:00