Leonardo de Moura
698754b2bb
feat(library/definitional/equations): display elaborated equation lhs's when there are missing cases
2015-01-08 12:00:47 -08:00
Leonardo de Moura
4e49e73585
refactor(library/init/logic): add inhabited related functions, rename inhabited.default to default
2015-01-07 18:45:58 -08:00
Leonardo de Moura
1fab144aa7
refactor(library/init/nat): rename constants
...
closes #387
2015-01-07 18:26:51 -08:00
Jeremy Avigad
50f03c5a09
refactor(library/data/nat/order): make nat order an instance of linear_ordered_semigroup, rename various theorems
2015-01-07 18:18:28 -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
fb1cb3c623
test(tests/lean/run): define tree_list length function using recursive equations
...
tree_list is part of a mutually inductive datatype.
2015-01-06 11:57:34 -08:00
Leonardo de Moura
559ee3e3e1
fix(util/buffer): bug in expand method
...
fixes #385
2015-01-06 11:42:40 -08:00
Leonardo de Moura
6451cad38d
test(tests/lean/run): define list head using recursive equations
2015-01-05 19:50:34 -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
cbae6a2ca0
test(tests/lean/run): define list filter function using recursive equations
2015-01-05 17:05:01 -08:00
Leonardo de Moura
a24a7f7fa1
test(tests/lean/run) define vector last and unzip functions using recursive equations
2015-01-05 17:04:55 -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
d8f3bcec67
feat(library/init/logic): add 'arbitrary'
...
It is identical to default, but it is opaque.
That is, when we use 'arbitrary A', we cannot rely on the particular
value selected.
2015-01-05 13:27:09 -08:00
Leonardo de Moura
0d84943d52
test(tests/lean/run): show that nat has decidable equality using recursive equations
2015-01-05 12:41:18 -08:00
Leonardo de Moura
fd332e411d
test(tests/lean/run): add more overlapping patterns examples
2015-01-05 12:25:14 -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
f07475667b
test(tests/lean/run): define vector map using recursive equations
2015-01-04 19:56:50 -08:00
Leonardo de Moura
7ff03e2846
test(tests/lean/run): define vector diagonal using recursive equations
2015-01-04 17:58:35 -08:00
Leonardo de Moura
7488378445
test(tests/lean/run): define list append using recursive equations
2015-01-04 17:58:24 -08:00
Leonardo de Moura
7fca862fc3
test(tests/lean/run): define fibonacci using recursive equations
2015-01-04 17:47:18 -08:00
Leonardo de Moura
faf78ce3e6
feat(library/definitional/equations): brec_on compilation
2015-01-04 17:45:13 -08:00
Leonardo de Moura
5bf8141af2
test(tests/lean/hott): add test to demonstrate limitations of the current compilation procedure
2015-01-02 23:18:35 -08:00
Leonardo de Moura
92b6c06a21
test(tests/lean/run): add basic pattern matching compilation test
2015-01-02 22:22:20 -08:00
Leonardo de Moura
c66826787a
test(tests/lean/run): add basic pattern matching compilation test
2015-01-02 22:07:31 -08:00
Leonardo de Moura
7f7d318b22
feat(library/definitional/equations): add dependent pattern matching compilation
2015-01-02 22:06:40 -08:00
Jeremy Avigad
1eea75b6fc
fix(library/data/nat/div,tests/lean/run/ppbeta): make decidable for dvd transparent, name change in ppbeta
2014-12-26 16:44:43 -05:00
Jeremy Avigad
25394dddb7
refactor(library): change mul.left_id to mul_one, and similarly for mul.right_id, add.left_id, add.right_id
2014-12-23 21:14:36 -05:00
Jeremy Avigad
486bc321ff
refactor(library/data/nat): rename theorems
2014-12-23 21:14:35 -05:00
Leonardo de Moura
2be83fbff7
test(tests/lean): remove data.nat dependency
2014-12-23 17:42:56 -08:00
Leonardo de Moura
264c88d332
test(tests/lean/hott): add tele_eq example using HoTT library
2014-12-22 09:43:16 -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
70f7ec3cf2
test(tests/lean/hott): add test for 'cases' tactic
2014-12-20 11:36:32 -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
2521dbb39e
refactor(hott): use same name convention for sigma in the HoTT and standard libraries
2014-12-19 18:46:06 -08:00
Leonardo de Moura
1e2fc54f2f
refactor(library/init/sigma): rename sigma.dpair->sigma.mk, sigma.dpr1->sigma.pr1, sigma.dpr2->sigma.pr2
2014-12-19 18:23:08 -08:00
Leonardo de Moura
9eea32b076
refactor(library/init/datatypes): change implicit arguments of sum.inl and sum.inr
2014-12-19 18:07:13 -08:00
Leonardo de Moura
07d7ea2f4e
refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean
2014-12-19 15:08:21 -08:00
Leonardo de Moura
1797e2846f
fix(tests/lean/run): replace "open [notation]" with "open [notations]"
2014-12-17 18:28:38 -08:00
Leonardo de Moura
43633085b9
fix(tests/lean): adjust tests to recent changes in the lean libraries
2014-12-16 13:28:43 -08:00
Leonardo de Moura
86f3d029c7
test(tests/lean/extra): more tests for equations compiler
2014-12-15 19:22:17 -08:00
Leonardo de Moura
abe129aa4f
refactor(library): rename theorems "iff.flip_sign -> not_iff_not_of_iff" and "decidable_iff_equiv -> decidable_of_decidable_of_iff"
2014-12-15 19:17:51 -08:00
Leonardo de Moura
5cf8064269
refactor(library): rename exists_elim and exists_intro to exists.elim
...
and exists.intro
2014-12-15 19:07:38 -08:00
Jeremy Avigad
3e9a484851
refactor(library/logic/connectives): rename theorems
2014-12-15 15:05:44 -05:00
Leonardo de Moura
c6ebe9456e
feat(library/data/nat): add "bounded" quantifiers
...
Later, we will add support for arbitrary well-founded relations
2014-12-13 15:42:38 -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
c291063f3a
fix(frontends/lean/structure_cmd): simplify structure names
2014-12-13 14:18:02 -08:00
Leonardo de Moura
c9365db41b
test(tests/lean/extra): more tests for equation elaborator
2014-12-12 15:43:41 -08:00
Leonardo de Moura
477d79ae47
refactor(library/init): move more theorems to logic
2014-12-12 13:50:53 -08:00
Leonardo de Moura
d6c8e23b03
refactor(library/init/logic): move theorems to library/logic
2014-12-12 13:24:17 -08:00
Leonardo de Moura
29aaa21f2a
fix(tests/lean/interactive): adjust test to reflect changes in the standard library
2014-12-11 19:53:41 -08:00
Leonardo de Moura
ab873cfff9
feat(frontends/lean/elaborator): replace metavariables in the equation lhs with fresh local constants before invoking compiler
2014-12-11 19:51:49 -08:00
Leonardo de Moura
b01cf73a91
feat(library/init/logic): add is_true and is_false
2014-12-11 18:14:03 -08:00
Leonardo de Moura
91ce99d921
feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion
2014-12-11 18:13:35 -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
Leonardo de Moura
4342454339
test(tests/lean/hott): add test for no_confusion construction for HoTT
2014-12-09 15:41:54 -08:00
Leonardo de Moura
05f27b8f0e
feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures
...
It seems most of the time these theorems are not used at all.
They are just polluting the namespace.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-09 12:40:09 -08:00
Leonardo de Moura
58432d0968
feat(library/definitional): add no_confusion construction that is compatible with the HoTT library
2014-12-08 22:11:48 -08:00
Leonardo de Moura
2bb51554d5
feat(library/definitional/util): add telescope equality for HoTT library
...
This is needed for implementing no_confusion for HoTT.
We can't use heterogeneous equality in HoTT.
2014-12-07 18:35:55 -08:00
Leonardo de Moura
466b671752
fix(tests/lean/interactive/coe): adjust test to reflect changes in the standard library
2014-12-05 22:27:03 -08:00
Leonardo de Moura
e72c4977f0
feat(frontends/lean): nicer notation for dependent if-then-else
2014-12-04 11:13:09 -08:00
Leonardo de Moura
ebda057499
fix(library/tactic/intros_tactic): seg fault at intros tactic, fixes #366
2014-12-04 09:26:10 -08:00
Leonardo de Moura
1a813fc720
test(tests/lean/run/nested_rec.lean): add nested recursion example based on well-founded recursion package
2014-12-03 22:11:01 -08:00
Leonardo de Moura
b6a1c118f4
fix(tests/lean/whnf): make sure the test does not produce 'sorry'
2014-12-03 21:12:33 -08:00
Leonardo de Moura
173e84c299
fix(tests/lean/struct_class): adjust test result to reflect recent changes
2014-12-03 20:32:33 -08:00
Leonardo de Moura
811bc6a31f
feat(library/init/measurable): add 'measurable' type class
2014-12-03 18:54:24 -08:00
Leonardo de Moura
e5fc0f90b2
test(tests/lean/run): try different ways to pack mutually recursive datatypes
2014-12-03 15:28:44 -08:00
Leonardo de Moura
9ae96514e0
test(tests/lean/run): use 'cases' tactic
2014-12-03 15:28:22 -08:00
Leonardo de Moura
d10bb92a7d
feat(library/aliases): protected definitions in nested namespaces, closes #331
2014-12-03 14:25:02 -08:00
Leonardo de Moura
0443c1e70c
fix(frontends/lean): intro tactic + universe variables, fixes #362
2014-12-03 12:56:30 -08:00
Leonardo de Moura
fca97d5bb2
feat(library/definitional): add brec_on construction, closes #272
2014-12-03 10:39:32 -08:00
Leonardo de Moura
06f436840f
fix(library/unifier): postpone class-instance constraints whose type could not be inferred
2014-12-01 22:27:23 -08:00
Leonardo de Moura
19d14678ef
refactor(library/unifier): remove dead code
2014-12-01 21:57:34 -08:00
Leonardo de Moura
e6672b958f
fix(library/tactic/inversion_tactic): add missing case
2014-12-01 19:11:44 -08:00
Leonardo de Moura
bc7ee2958f
fix(library/tactic/inversion_tactic): bug in mutually recursive case
2014-12-01 18:32:38 -08:00
Leonardo de Moura
8137f94b3c
fix(tests/lean): to reflect recent changes
2014-12-01 17:14:11 -08:00
Leonardo de Moura
6640fbf11b
feat(library/definitional/brec_on): simplify universe level constraints for non-reflexive recursive datatypes
2014-12-01 17:11:06 -08:00
Leonardo de Moura
320971832d
feat(frontends/lean/pp): add hard-coded pretty printer for nat numerals
2014-12-01 16:07:55 -08:00
Leonardo de Moura
263424b0fd
test(tests/lean/slow): add "manual" 'path induction' tactic
2014-12-01 13:50:01 -08:00
Leonardo de Moura
193fed7061
fix(library/tactic/inversion_tactic): uninitialized variable
2014-11-30 22:41:22 -08:00
Leonardo de Moura
eefe03cf56
fix(tests/lean): adjust tests to modifications to standard library
2014-11-30 21:16:01 -08:00
Leonardo de Moura
dad94eafbe
refactor(data/nat/decl): use new naming convention at data/nat/decl.lean
2014-11-30 15:07:09 -08:00
Leonardo de Moura
079bf7f633
test(tests/lean/run/vector): use nat.add
2014-11-30 13:53:02 -08:00
Leonardo de Moura
c08f4672e4
feat(library/tactic): add 'assert' tactic, closes #349
2014-11-29 21:34:49 -08:00
Leonardo de Moura
1a7dd56f0f
fix(library/tools/tactic): 'cases' argument precedence
2014-11-29 21:03:45 -08:00
Leonardo de Moura
f51fa93292
feat(library/tactic): add 'fapply' tactic, closes #356
2014-11-29 19:20:41 -08:00
Leonardo de Moura
2c0472252e
feat(frontends/lean): allow expressions to be used to define precedence, closes #335
2014-11-29 18:29:48 -08:00
Leonardo de Moura
2487e3b83d
fix(frontends/lean/parser): user provided numeral notation should have precedence over the default based on 'num'
2014-11-29 17:29:03 -08:00
Leonardo de Moura
bc65aeb5e1
fix(frontends/lean/calc): add expected type for single-step calc expressions, fixes #357
...
This is not an issue for calc expressions containing multiple steps,
since the transitivity step will "force" the expected type for the proofs.
2014-11-29 15:35:09 -08:00
Leonardo de Moura
6fbbf66565
test(tests/lean/run/vector): define 'map' on vector using brec_on and new inversion tactic
2014-11-29 13:28:01 -08:00
Leonardo de Moura
a0d650d9cc
fix(library/tactic/inversion_tactic): complete 'deletion' transition
2014-11-29 09:36:41 -08:00
Leonardo de Moura
7000365a04
fix(tests/lean): to reflect changes in the standard library
2014-11-28 23:03:37 -08:00
Leonardo de Moura
e0debca771
feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses
2014-11-28 22:25:37 -08:00
Leonardo de Moura
22b2f3c78c
fix(library/tactic/inversion_tactic): bug in injectivity transition
2014-11-28 22:07:35 -08:00
Leonardo de Moura
a6be460166
feat(library/tactic/inversion_tactic): basic 'inversion' tactic
2014-11-28 21:56:13 -08:00
Leonardo de Moura
f7deabfd19
feat(library/rename): add notation for rename
2014-11-26 19:02:11 -08:00
Leonardo de Moura
e55397d422
feat(library/tactic): add 'clears' and 'reverts' variants
2014-11-26 14:49:48 -08:00
Leonardo de Moura
2bd8f969d5
feat(library/tactic): add 'revert' tactic, closes #346
2014-11-26 14:23:42 -08:00
Leonardo de Moura
c28e9b9234
feat(library/tactic): add 'clear' tactic, closes #341
2014-11-26 13:11:36 -08:00
Leonardo de Moura
ffdeb0edc4
fix(frontends/lean/elaborator): unsolved metavariables, fix #329
2014-11-26 11:56:39 -08:00
Leonardo de Moura
df51ba8b7c
feat(library/definitional/projection): use strict implicit inference, closes #344
2014-11-25 18:04:06 -08:00
Leonardo de Moura
edc9e4908c
test(tests/lean/run): add another subterm example
2014-11-25 16:53:09 -08:00
Leonardo de Moura
f737a140c1
test(tests/lean/run): direct subterm for non-reflexive datatype
2014-11-25 16:22:11 -08:00
Leonardo de Moura
ef75cac1c0
feat(kernel/expr): change the rules for inferring implicit arguments, closes #344
2014-11-25 12:54:07 -08:00
Leonardo de Moura
24a15b6c46
fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343
2014-11-24 21:33:52 -08:00
Leonardo de Moura
f729762c23
test(tests/lean/run): add test for well_founded relation for mutually recursive datatypes
2014-11-24 14:58:30 -08:00
Leonardo de Moura
d81a6259e8
feat(frontends/lean/find_cmd): add options for controlling find_decl
2014-11-24 00:16:10 -08:00
Leonardo de Moura
f1e915a188
feat(frontends/lean): add 'find_decl' command
2014-11-23 23:00:59 -08:00
Leonardo de Moura
44a2ef8f6f
fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file
2014-11-23 17:49:14 -08:00
Leonardo de Moura
64686c1278
feat(frontends/lean): allow user to associate precedence to binders, closes #323
2014-11-23 17:30:46 -08:00
Leonardo de Moura
cf3b0e1087
feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333
2014-11-23 17:30:46 -08:00
Leonardo de Moura
13fba433b0
feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327
2014-11-23 17:30:22 -08:00
Leonardo de Moura
919007612a
fix(tests/lean): adjust tests since module 'logic' depends on nat
...
We need that because of the definitional package
2014-11-22 17:34:05 -08:00
Leonardo de Moura
5db13da95f
test(tests/lean/run/div_wf): cleanup div based on well founded recursion
2014-11-22 09:56:47 -08:00
Leonardo de Moura
064ecd3e3d
refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package
...
We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
2014-11-22 00:19:39 -08:00
Leonardo de Moura
5d5fd2da50
fix(frontends/lean): tactic + section variables, fixes #332
2014-11-21 10:07:16 -08:00
Leonardo de Moura
7e7e7c241c
test(tests/lean/run/gcd): gcd compiled by hand into wf recursion
2014-11-18 19:34:01 -08:00
Leonardo de Moura
4fbb5cfcca
test(tests/lean/run/div_wf): cleanup
2014-11-18 17:59:14 -08:00
Leonardo de Moura
a065c7bf96
test(tests/lean/run/tree_height): experiment with wf relation based on the height
...
This is easier to generate than the subterm relation
2014-11-18 17:57:17 -08:00
Leonardo de Moura
5fbe990c7a
test(tests/lean/run): define div using wf package
2014-11-18 13:55:58 -08:00
Leonardo de Moura
5daff18017
test(tests/lean/run): pre-quotient experiment
2014-11-17 18:30:11 -08:00
Leonardo de Moura
28c63e685b
feat(frontends/lean): add '[local]' notation, closes #322
2014-11-16 21:15:04 -08:00
Leonardo de Moura
bf5f48730c
refactor(library/data/subtype): define subtype using 'structure' command
2014-11-16 15:01:14 -08:00
Leonardo de Moura
a171f8fbc3
test(tests/lean/run): simple diag for square matrices
2014-11-15 18:49:17 -08:00
Leonardo de Moura
1b95b69251
test(tests/lean/run): define subterm relation for vectors
2014-11-15 16:17:51 -08:00
Leonardo de Moura
ea640257bf
feat(frontends/lean/structure_cmd): generate no_confusion for structures too
2014-11-15 16:00:09 -08:00
Leonardo de Moura
b87559dac5
test(tests/lean/run): define subterm relation for trees by hand
2014-11-15 13:29:23 -08:00
Leonardo de Moura
7685516d1e
feat(frontends/lean): better default for atomic notation
2014-11-14 16:25:13 -08:00
Leonardo de Moura
67de3b06f3
feat(kernel/level): improve universe level pretty printer
...
Example: produce `l+2` instead of `succ (succ l)`.
2014-11-14 14:51:03 -08:00
Leonardo de Moura
00df34a1c4
feat(library/unifier): generalize method process_succ_eq_max_core
2014-11-14 14:25:41 -08:00
Leonardo de Moura
488f989c46
fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop
2014-11-14 13:57:42 -08:00
Leonardo de Moura
58525905d0
fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command
2014-11-13 22:05:55 -08:00
Leonardo de Moura
51719145f9
feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2)
2014-11-12 17:28:33 -08:00
Leonardo de Moura
edd04881ee
fix(library/logic): import prod and unit declarations in logic
...
Reason: we need them for automatically generating constructions needed
by the definitional package
2014-11-12 16:54:50 -08:00
Leonardo de Moura
6bc89f0916
feat(library/definitional): define ibelow and below
...
These are helper definitions for brec_on and binduction_on
2014-11-12 16:38:46 -08:00
Leonardo de Moura
97609d1625
test(tests/lean/run/nateq): add example that triggered previous modification
2014-11-12 15:11:08 -08:00
Leonardo de Moura
b07b82cf43
fix(library/definitional): marking cases_on and rec_on as reducible
...
The idea is to avoid counter-intuitive behavior
2014-11-12 15:03:30 -08:00
Leonardo de Moura
a3066e3eaa
fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator
2014-11-12 13:10:19 -08:00
Leonardo de Moura
463e70332d
test(tests/lean/run): define brec_on and binduction_on for a reflexive type
...
We say an inductive type T is reflexive if it contains at least one constructor that
takes as an argument a function returning T.
For reflexive types it doesn't seen to be possible to define a single
brec_on that can eliminate to Type.{>=1} and Prop.
The universe level expressions get too complicated.
Even if we extend the universe constraint solver in the kernel, the
additional complexity might be a problem.
We workaround this issue by defining two versions of brec_on:
- One (brec_on) that eliminates to Type.{>=1}, and
- binduction_on that eliminates to Prop.
For non-reflexive types, we can combine both of them.
2014-11-12 10:52:32 -08:00
Leonardo de Moura
5312afa7ec
feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes
...
The new test contains examples that required explicit levels.
2014-11-12 10:52:32 -08:00
Leonardo de Moura
faf90c4b87
test(tests/lean/run): test brec_on on vectors
2014-11-11 17:23:59 -08:00
Leonardo de Moura
f6889951c6
fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion
2014-11-11 15:14:08 -08:00
Leonardo de Moura
e65b5884e5
test(tests/lean/run/forest): define brec_on for forests
...
Almost everything explicit to get an idea of what needs to be generated automatically.
2014-11-11 13:16:23 -08:00
Leonardo de Moura
b3e4a689cf
test(tests/lean/run): define ackermann function using recursors
2014-11-11 11:06:10 -08:00
Leonardo de Moura
e2ce942513
fix(tests/lean): adjust test to new eval
semantics
2014-11-10 21:10:33 -08:00
Leonardo de Moura
1f92751c4d
test(tests/lean/run): fibonacci using well_founded recursion
2014-11-10 12:46:55 -08:00
Leonardo de Moura
363d4a7577
fix(library/definitional/no_confusion): assertion violation
2014-11-10 10:32:03 -08:00
Leonardo de Moura
fa26c2301c
fix(frontends/lean): fix pretty-printing spacing problem
2014-11-09 14:49:43 -08:00
Leonardo de Moura
3aac26d658
fix(frontends/lean): tactic + variables bug, fixes #315
2014-11-09 14:43:22 -08:00
Leonardo de Moura
eff3c6b774
feat(frontends/lean): add variation of the foldl/foldr notation where initial element is suppressed, closes #314
...
See tests/lean/fold.lean for examples
2014-11-09 14:08:33 -08:00
Leonardo de Moura
ce889ddf60
feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'
2014-11-09 12:55:13 -08:00
Leonardo de Moura
df5a17cdce
feat(frontends/lean/placeholder_elaborator): include type in class-instance resolution trace
2014-11-09 12:06:16 -08:00
Leonardo de Moura
9b9ae128d5
feat(frontends/lean): include file-name and line/col numbers when displaying class-instance resolution trace
2014-11-09 11:47:01 -08:00
Leonardo de Moura
aef1dd9a04
test(tests/lean/run): fibonacci using below_rec_on (aka brec_on)
2014-11-08 22:19:18 -08:00
Leonardo de Moura
1b6e40d3d6
test(tests/lean/run): define below_rec_on (aka brec_on) for vectors
2014-11-08 22:19:18 -08:00
Leonardo de Moura
e8bc0f8249
feat(library/defitional): add no_confusion construction for inductive datatypes that are not propositions
2014-11-08 18:56:52 -08:00
Leonardo de Moura
b5da143fc0
feat(library/defitional): add no_confusion_type construction for inductive datatypes that are not propositions
2014-11-08 15:20:19 -08:00
Leonardo de Moura
c7992f2cac
feat(frontends/lean): add [whnf] modifier to eval command
2014-11-08 10:19:29 -08:00
Leonardo de Moura
f16f215c2a
refactor(data/num/string): break into pieces to reduce dependencies
2014-11-07 08:53:14 -08:00
Leonardo de Moura
e993486301
refactor(library/data/num): break into pieces to reduce dependencies
2014-11-07 08:24:29 -08:00
Leonardo de Moura
b5e0ded163
feat(frontends/lean): max precedence used by Lean is not max_uint anymore
...
The motivation is to allow users to define notation with higher
precedence than function application.
2014-11-07 07:57:11 -08:00
Leonardo de Moura
85d0521d48
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
2014-11-06 21:34:05 -08:00
Leonardo de Moura
781f709bb4
feat(library/logic): import wf.lean in logic/default.lean
...
We will use well-founded recursion in the definitional package
2014-11-06 15:03:13 -08:00
Leonardo de Moura
4fa363adbf
fix(tests/lean): avoid 'sorry' in expected output
2014-11-06 14:06:55 -08:00
Leonardo de Moura
af88e34588
fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop
2014-11-06 14:03:28 -08:00
Leonardo de Moura
be52d950f0
fix(frontends/lean): improve error message, addresses issue #299
2014-11-06 12:19:40 -08:00
Leonardo de Moura
e499f8e20a
feat(kernel/inductive): relax conditions for an inductive datatype in Prop to be able to eliminate into Type
...
The new relaxed version allows us to define the "accessability"
proposition and have an eliminator into Type.
See justification in the new comments at inductive.cpp
2014-11-06 09:36:54 -08:00
Leonardo de Moura
8723f5b613
fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.
...
Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).
This bug would confuse users and make them believe they define something
different.
2014-11-05 23:12:00 -08:00
Leonardo de Moura
b3ad8c704a
feat(frontends/lean/structure_cmd): allow inheritance from two identical structures, closes #296
2014-11-05 15:01:05 -08:00
Leonardo de Moura
4650791108
feat(frontends/lean): add 'print fields' command
2014-11-05 14:06:54 -08:00
Leonardo de Moura
354baf4d13
test(tests/lean/run): add structure command test
2014-11-05 12:54:03 -08:00
Leonardo de Moura
f8a2bc41a5
fix(frontends/lean/structure_cmd): bad test output
2014-11-05 12:02:53 -08:00
Leonardo de Moura
677e0aeef6
fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified
2014-11-05 12:02:52 -08:00
Leonardo de Moura
defc2478b5
feat(frontends/lean): add 'record' as an alias for 'structure' command
2014-11-05 12:02:52 -08:00
Leonardo de Moura
5b87d060cf
fix(frontends/lean/structure_cmd): universe level validation
2014-11-04 22:19:23 -08:00
Leonardo de Moura
6944c7d902
fix(frontends/lean/placeholder_elaborator): local context must be adjusted when performing class-instance resolution modulo Pi-abstraction, fixes #293
2014-11-04 18:41:27 -08:00
Leonardo de Moura
3bfe5b0b7e
fix(frontends/lean): type information for "atomic" notation declaration, fixes #292
2014-11-04 18:01:20 -08:00
Leonardo de Moura
d58c3e498d
feat(frontends/lean/builtin_cmds): add 'print prefix' command
2014-11-04 08:40:32 -08:00
Leonardo de Moura
3454e70017
fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289
...
Fix incorrect line/column number information in error messages produced
during inductive datatype elaboration.
2014-11-04 07:44:47 -08:00
Leonardo de Moura
b6722a5d33
feat(frontends/lean/structure_cmd): add 'private' modifier for parent structures
...
When it is used coercions/instances to parent structure are to registered
2014-11-03 23:16:49 -08:00
Leonardo de Moura
b24165dc7b
feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on'
2014-11-03 23:06:33 -08:00
Leonardo de Moura
7897e21a14
feat(frontends/lean/structure_cmd): allow fields to be suppresed, but constructor to be provided
2014-11-03 22:55:51 -08:00
Leonardo de Moura
08b4ce2db9
feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided
2014-11-03 22:40:08 -08:00
Leonardo de Moura
8f3139231b
feat(frontends/lean/structure_cmd): allow structure declarations that contains only a header
2014-11-03 22:17:43 -08:00
Leonardo de Moura
91749d2364
fix(frontends/lean/structure_cmd): modify coercion generation
...
The previous coercion was more efficient, but the computation was
getting stuck when processing algebraic structures
2014-11-03 19:37:11 -08:00
Leonardo de Moura
d2b5af237e
refactor(library): use new 'structure' command to define prod and sigma
2014-11-03 18:57:55 -08:00
Leonardo de Moura
ea7470375f
fix(tests/lean): to reflect changes in the standard library
2014-11-03 18:46:53 -08:00
Leonardo de Moura
c306bfa83c
feat(frontends/lean/structure_cmd): add 'eta' theorem for structures
2014-11-03 18:33:44 -08:00
Leonardo de Moura
186d910d0b
feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes)
2014-11-03 17:55:59 -08:00
Leonardo de Moura
9531203d9d
feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used
2014-11-03 17:47:08 -08:00
Leonardo de Moura
b112f3c582
feat(frontends/lean/structure_cmd): add coercions to parent structures
2014-11-03 17:39:52 -08:00
Leonardo de Moura
7afa69577e
feat(frontends/lean/structure_cmd): add aliases for structure decls
2014-11-03 15:50:41 -08:00
Leonardo de Moura
efe1105eb9
fix(frontends/lean): alias generation for composite names was not working
...
This is an issue for declarations that generate composite names such as
the inductive datatype packacke.
The commit also fix a bug in the generate of aliases for recursors
2014-11-03 15:43:58 -08:00
Leonardo de Moura
594e3ea8fc
fix(frontends/lean/structure_cmd): 'rec' must be marked as protected
2014-11-03 14:50:12 -08:00
Leonardo de Moura
0f56b5f5b7
test(tests/lean/run): add structure command test
2014-11-03 14:29:17 -08:00
Leonardo de Moura
a2e75159c8
fix(frontends/lean): process choice-exprs at check_constant_next
2014-11-02 19:42:30 -08:00
Leonardo de Moura
c7406d6ce8
fix(library/scoped_ext): bug when declaring nested namespaces
2014-11-02 15:35:49 -08:00
Leonardo de Moura
df008dc3c3
feat(frontends/lean/inductive_cmd): create a namespace for each declared datatype
2014-11-01 19:15:46 -07:00
Leonardo de Moura
ea55ec4090
feat(frontends/lean/decl_cmds): remove useless name from 'example' commad
2014-11-01 16:12:23 -07:00
Leonardo de Moura
1e6f7cdbb4
chore(frontends/lean/decl_cmds): add 'example' command
...
It is like a theorem, but it is discarded after checking
2014-11-01 11:37:39 -07:00
Leonardo de Moura
94cf10284a
fix(frontends/lean/calc_proof_elaborator): bug when inserting symmetry proofs for heq, fixes #286
...
The problem was that heq type is
Pi {A : Type} (a : A) {B : Type} (b : B), Prop
The calc_proof_elaborator was assuming that (a : A) (b : B) were the
last two arguments in any relation supported by calc.
The fix is to remove this assumption.
2014-11-01 07:30:04 -07:00
Leonardo de Moura
2688ca38bf
feat(frontends/lean/inductive_cmd): notation for enumeration types
2014-10-31 19:01:32 -07:00
Leonardo de Moura
57b19b787b
feat(frontends/lean/calc_proof_elaborator): when 'elaborator.calc_assistant' is on, generate same info that is generated if !
was used
2014-10-31 09:49:45 -07:00
Leonardo de Moura
dc7ab17d2a
feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option
2014-10-31 09:49:45 -07:00
Leonardo de Moura
d7beabe91c
fix(frontends/lean/calc_proof_elaborator): improve calc proof assistant
2014-10-31 09:49:45 -07:00
Leonardo de Moura
17df85f592
feat(frontends/lean/calc_proof_elaborator): add '{...}' if needed in calc proof steps
...
This is part of #268
2014-10-31 00:55:19 -07:00
Leonardo de Moura
591e566472
feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator
...
This is part of #268
2014-10-30 23:24:09 -07:00
Leonardo de Moura
c5a62f8abb
feat(frontends/lean): insert !
in calculational proofs when needed
...
This is part of #268
2014-10-30 22:22:04 -07:00
Leonardo de Moura
b87764eaf6
test(tests/lean): add unique class instance resolution test
2014-10-30 14:50:32 -07:00
Leonardo de Moura
64c3ba7b74
feat(frontends/lean): display metavariable application arguments in check command
...
The idea is to "fix" counter-intuitive output like the ones were
produced in the tests check.lean and check2.lean
2014-10-30 13:28:25 -07:00
Leonardo de Moura
dcd7e53fa7
feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command
...
We don't need it anymore after previous commit 2a16050
2014-10-30 13:12:45 -07:00
Leonardo de Moura
2a160508c3
feat(frontends/lean): lean --server
should display meta-variables using the approach used in check command, closes #280
2014-10-30 12:45:41 -07:00
Leonardo de Moura
a1ea087f8e
fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element
2014-10-30 10:35:45 -07:00
Leonardo de Moura
84b516994c
fix(library/tactic): type check generalization result, fixes #273
2014-10-29 20:34:01 -07:00
Leonardo de Moura
6107da05db
fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283
2014-10-29 19:47:14 -07:00
Leonardo de Moura
d7ded15486
fix(tests/lean/interactive): modify to reflect recent changes
2014-10-29 19:44:53 -07:00
Leonardo de Moura
9547e2d077
feat(library/tactic): add rotate_left/rotate_right tactics, closes #278
2014-10-29 19:13:55 -07:00
Leonardo de Moura
a98b12f067
fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276
2014-10-29 16:51:06 -07:00
Leonardo de Moura
88d55bfef0
fix(library/definitional/projection): remove redundant 'error in'
2014-10-29 16:51:06 -07:00
Leonardo de Moura
30571ce418
fix(library/definitional/projection): error messages for projection generation
2014-10-29 13:39:17 -07:00
Leonardo de Moura
fe4ea48381
feat(library/definitional/projection): add projection generator, closes #257
2014-10-29 13:13:05 -07:00
Leonardo de Moura
e22eb3543c
feat(library/tactic): add whnf tactic, closes #270
2014-10-28 23:18:49 -07:00
Leonardo de Moura
83e4c0fcec
feat(frontends/lean): hide tactic "types"
...
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
2014-10-28 22:38:10 -07:00
Leonardo de Moura
eeb6c72508
feat(frontends/lean): modify begin-end
semantics, closes #258
2014-10-28 22:15:38 -07:00
Leonardo de Moura
1c2bbcfebc
feat(frontends/lean/info_manager): add separator --
when displaying PROOF_STATE info
...
This feature was implemented to address issue #259
2014-10-28 16:39:21 -07:00
Leonardo de Moura
186e598bf8
feat(library/tactic/goal): add option pp.compact_goals
2014-10-28 16:30:37 -07:00
Leonardo de Moura
ea739100b3
fix(library/unifier): broken optimization in the unifier
...
See new comments and tests for details.
2014-10-28 16:09:41 -07:00
Leonardo de Moura
777aa63660
fix(kernel/inductive): relax eliminator generation rules for empty types
...
This commit also removes the workaround false.rec_type. It is not needed anymore
2014-10-28 10:31:00 -07:00
Leonardo de Moura
60f32fa709
fix(frontends/lean): begin-end
automatic tactic notation bug, fixes #262
2014-10-27 17:12:25 -07:00
Leonardo de Moura
78bc3ef7e4
feat(library/unifier): improve FailLocal/FailCircular failures in the unifier by using normalization
...
This improvements was marked as TODO, and was preventing us from
elaborating the example in the new test vector3.lean
2014-10-27 16:49:29 -07:00
Leonardo de Moura
7516fcad97
feat(kernel/type_checker): add is_stuck
method, and improve ensure_pi method, closes #261
2014-10-27 13:16:50 -07:00
Leonardo de Moura
49941ce35b
test(tests/lean/run/sigma_no_confusion): define 'no_confusion' for sigma types
2014-10-27 07:26:01 -07:00
Leonardo de Moura
d66e5a6c41
fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming
2014-10-26 19:19:45 -07:00
Leonardo de Moura
81dc201bab
fix(frontends/lean/elaborator): nested begin-end bug
2014-10-26 18:23:30 -07:00
Leonardo de Moura
a544d32fcf
fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders
2014-10-26 16:11:58 -07:00
Leonardo de Moura
cc6a96e8ba
fix(frontends/lean): improve begin-end construct
2014-10-26 15:47:29 -07:00
Leonardo de Moura
fd60cf6a79
feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification
...
See new node.inj4 theorem, we need the extra power to be able to avoid type information at
exact (assume e₁ e₂, e₁)
2014-10-26 10:27:33 -07:00
Leonardo de Moura
8e6de93394
fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant
2014-10-26 09:47:11 -07:00
Leonardo de Moura
c7f6a6b94e
feat(library/definitional/cases_on): automatically add 'cases_on'
2014-10-25 17:22:02 -07:00
Leonardo de Moura
cdcde661ef
feat(library/definitional/induction_on): automatically add 'induction_on'
2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
2014-10-25 13:08:59 -07:00
Leonardo de Moura
7a033ac07e
feat(frontends/lean): add 'print axioms' command, close #251
2014-10-24 14:35:03 -07:00
Leonardo de Moura
db25f933b0
feat(frontends/lean): use nice names for meta-variables when executing check c
and c
is a constant
2014-10-24 08:23:26 -07:00
Leonardo de Moura
79d0347721
feat(library/tactic): add generalize tactic, closes #34
...
Remark: the intros tactic has been added in a different commit: 7d0100a340
2014-10-23 22:40:15 -07:00
Leonardo de Moura
b83b065d00
feat(library/tactic/apply_tactic): modify heuristic for adding arguments to apply tactic.
2014-10-23 22:36:32 -07:00
Leonardo de Moura
f027acb5cb
fix(frontends/lean): missing type info in expressions nested in tactics
2014-10-23 18:31:05 -07:00
Leonardo de Moura
212ae0b61c
feat(frontends/lean): automatically add 'info' tactic in begin-end blocks
...
Actually, the tactic is only added when Lean is in collect-info mode.
2014-10-23 13:30:04 -07:00
Leonardo de Moura
e750c9b67a
feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode
2014-10-23 13:18:30 -07:00
Leonardo de Moura
38a9aa2a98
feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions
2014-10-23 10:26:19 -07:00
Leonardo de Moura
00f9a10e82
refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic
...
This change also enabled us to remove hacks used in the tests modified
by this commit.
2014-10-23 10:26:19 -07:00
Leonardo de Moura
5a553603d1
fix(library/general_notation): mark \tr as left associative
2014-10-22 22:18:40 -07:00
Leonardo de Moura
c50227ea6e
feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included
...
This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
2014-10-22 18:11:09 -07:00
Leonardo de Moura
e95c7c5f70
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-22 17:29:50 -07:00
Leonardo de Moura
5e15ac0c92
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
2014-10-22 17:29:50 -07:00
Leonardo de Moura
323715e951
refactor(library/tactic): move 'tracing' tactics to separate module
2014-10-22 14:12:45 -07:00
Leonardo de Moura
33f18b9454
fix(kernel/converter): remove buggy eta-reduction and rely only on eta-expansion
...
The bug is exposed by new unit test
2014-10-21 16:54:25 -07:00
Leonardo de Moura
6b89080b1a
feat(frontends/lean): do not allow user to define notation using tokens !
and @
, closes #248
2014-10-21 16:28:36 -07:00
Leonardo de Moura
e24225fabf
feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations
2014-10-21 15:39:47 -07:00
Leonardo de Moura
6c7e23ecaa
refactor(library): use 'reserve' notation in the standard library
2014-10-21 15:39:47 -07:00
Leonardo de Moura
bb953b80aa
feat(frontends/lean): reserve notation, closes #95
2014-10-21 15:39:47 -07:00
Leonardo de Moura
8a44dfc1df
fix(frontends/lean/pp): bug in pretty printer notation match procedure
2014-10-20 18:58:27 -07:00
Leonardo de Moura
40fb66bf07
feat(frontends/lean): change default precedence to 1
2014-10-20 18:40:55 -07:00
Leonardo de Moura
e2fa981e89
fix(frontends/lean/pp): avoid parentheses around atomic notation
2014-10-20 18:08:13 -07:00
Leonardo de Moura
e68007a727
fix(frontends/lean/builtin_tactics): adjust tactics precedence
2014-10-20 17:10:16 -07:00
Leonardo de Moura
9b8f60b739
feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block
...
This is useful when debugging proofs.
2014-10-20 15:59:49 -07:00
Leonardo de Moura
c09bb3cc6f
fix(tests/lean/notation): remove 'sorry' warning from expected outputs
2014-10-20 15:34:44 -07:00
Leonardo de Moura
7d0100a340
feat(library/tactic): add 'intros' tactic
2014-10-20 15:26:16 -07:00
Leonardo de Moura
f0cc17af87
fix(frontends/lean/elaborator): missing type information when !
operator (aka consume_args) is used
2014-10-20 08:31:36 -07:00
Leonardo de Moura
a1006073d4
feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence
2014-10-19 13:39:06 -07:00
Leonardo de Moura
4d4bc0551f
feat(frontends/lean/pp): minimize number of spaces when pretty printing notation
2014-10-19 13:08:15 -07:00
Leonardo de Moura
ed1afe26bd
feat(frontends/lean/pp): support scopedexpr notation in the pretty printer
2014-10-19 12:50:40 -07:00
Leonardo de Moura
f63d47fef3
feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer
2014-10-19 11:16:24 -07:00
Leonardo de Moura
eef1cc4ac2
fix(frontends/lean/pp): implicit arguments in notation
2014-10-19 09:04:43 -07:00
Leonardo de Moura
555d26aa61
feat(frontends/lean/pp): take notation declarations into account when pretty printing
...
TODO: support foldl/foldr and binders
2014-10-19 08:41:29 -07:00
Leonardo de Moura
10b880ce3b
perf(kernel/metavar): improve occurs_expr and occurs performance
2014-10-17 14:05:22 -07:00
Leonardo de Moura
c4f02bd16a
refactor(kernel/expr): remove dead code
2014-10-16 13:09:26 -07:00
Leonardo de Moura
28128e0330
fix(frontends/lean): EXTRA_TYPE info
2014-10-16 12:25:18 -07:00
Leonardo de Moura
e6606ef2ac
feat(library/tactic): add 'rename' hypothesis tactic
2014-10-14 18:19:34 -07:00
Leonardo de Moura
90dba868e3
feat(library/tactic/proof_state): apply substitutions when pretty printing state
2014-10-14 17:37:20 -07:00
Leonardo de Moura
58c9421bab
refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44 , fixes #70
2014-10-14 17:18:40 -07:00
Leonardo de Moura
d75a9c840c
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
2014-10-13 21:08:36 -07:00
Leonardo de Moura
b7c1b348d1
feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration
2014-10-13 20:53:09 -07:00
Leonardo de Moura
08c0fb3a64
test(tests/lean/run): expand tree example
2014-10-13 07:08:29 -07:00
Leonardo de Moura
5c1d5133dd
fix(library/data/prod): make the notation for tuples and product types consistent
2014-10-13 06:48:37 -07:00
Leonardo de Moura
a26618e0f2
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
2014-10-12 13:06:00 -07:00
Leonardo de Moura
549f24335e
feat(frontends/lean): do not allow coercion definition in sections
2014-10-11 18:41:17 -07:00
Leonardo de Moura
158682219f
feat(frontends/lean): allow parameters only in contexts
2014-10-11 17:13:56 -07:00
Leonardo de Moura
f984b51291
feat(frontends/lean/notation_cmd): remove the cleanup notation hack
2014-10-11 16:40:26 -07:00
Leonardo de Moura
ca632cca13
feat(frontends/lean): add 'universe variable' command
...
We can declare variables anywhere. So, we must also be able do declare
"universe" variables anywhere. Here is a minimal example that requires
this feature
```
-- We want A and B to be in the same universe
universe variable l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
The following doesn't work because A and B are in different universes
```
variable A : Type
variable B : Type
definition tst := A = B
```
The following works, but tst is not universe polymorphic, since l is
one *fixed* global universe
```
universe l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
2014-10-11 14:22:33 -07:00
Leonardo de Moura
b0f8d86f26
feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242
2014-10-10 18:08:03 -07:00
Leonardo de Moura
5e6ff3eef3
fix(frontends/lean/elaborator): bug when reporting error position
2014-10-10 17:31:12 -07:00
Leonardo de Moura
f0523a3465
feat(frontends/lean): namespaces also define scope for variables
2014-10-10 16:21:30 -07:00
Leonardo de Moura
0641ee33ce
feat(frontends/lean): allow variables anywhere
2014-10-10 16:16:19 -07:00
Leonardo de Moura
3d65b1c25c
fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241
2014-10-10 15:41:55 -07:00
Leonardo de Moura
235b8975d2
feat(kernel/inductive): K-like reduction in the kernel
...
Given (H_1 : a = a), we have that
eq.rec H_2 H_1
reduces to H_2
This is not exclusive to equality.
It applies to any inductive datatype in Prop, containing only one
constructor with zero "arguments" (we say they are nullary).
BTW, the restriction to only one constructor is not needed, but it is
does not buy much to support multiple nullary constructors since Prop is
proof irrelevant.
2014-10-10 14:37:45 -07:00
Leonardo de Moura
402a351937
feat(frontends/lean): add 'universes' command
2014-10-10 08:45:59 -07:00
Leonardo de Moura
9ba59c6b25
feat(library/universe): improve support for universe level constraints in the unifier
2014-10-09 20:28:39 -07:00
Leonardo de Moura
8f1b6178a7
chore(*): minimize the use of parameters
2014-10-09 07:13:06 -07:00
Leonardo de Moura
8c5d3392c7
fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests
2014-10-08 23:44:09 -07:00
Leonardo de Moura
8947bf4347
feat(frontends/lean): display type of binders, closes #238
2014-10-08 22:54:10 -07:00
Leonardo de Moura
25fd370c51
fix(frontends/lean): bug when using nested sections and parameters
...
see tests/lean/run/section4.lean
2014-10-08 22:23:20 -07:00
Leonardo de Moura
57c85221fe
fix(frontends/lean): collect used universe levels after elaboration in the check command
2014-10-08 22:23:19 -07:00
Leonardo de Moura
eab9321a3b
fix(frontends/lean): make all variables/parameters visible for 'variables' command
2014-10-08 22:23:19 -07:00
Leonardo de Moura
757cb46579
test(tests/lean/run): add no_confusion test
2014-10-08 22:23:19 -07:00
Leonardo de Moura
3b23bec25b
feat(frontends/lean): variables/parameters and check commands have access to all section variables/parameters, closes #231
2014-10-08 08:40:55 -07:00
Leonardo de Moura
744cee8dd8
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228
2014-10-07 18:02:15 -07:00
Leonardo de Moura
d8572e249d
feat(frontends/lean/builtin_cmds): add 'print classes' command
2014-10-07 17:30:57 -07:00
Leonardo de Moura
90ece4dd1b
feat(frontends/lean): remove tactic hints for specific classes
...
The idea is to separate class-instance resolution and tactic framework
as two independent engines.
2014-10-07 09:44:01 -07:00
Soonho Kong
e41573afc4
chore(tests/*/test.sh): change working dir; avoid using ls in for-loop
2014-10-06 11:20:13 -07:00
Leonardo de Moura
f7e1b67f6c
test(tests/lean/run/print): add tests for 'print' cmd
2014-10-05 19:06:29 -07:00
Leonardo de Moura
a0d4d82f3f
refactor(data/nat/order): use new policy for marking implicit arguments and '!' operator
2014-10-05 11:36:39 -07:00
Leonardo de Moura
73aa024c31
refactor(library/logic): remove 'core' subdirectory
2014-10-05 10:50:13 -07:00
Leonardo de Moura
317e910054
refactor(library/data/bool): use new style
2014-10-05 09:50:55 -07:00
Leonardo de Moura
60d8369688
fix(library/unifier): missing justification when updating choice constraints
...
The bug was not producing incorrect results, but really bad error
messages.
See: empty.lean.expected.out
2014-10-04 10:40:53 -07:00
Leonardo de Moura
64f6601fe3
fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost
2014-10-04 09:15:42 -07:00
Leonardo de Moura
7073f036d8
test(tests/lean/run): add additional tests for section parameter/variable and strict implicit argument
2014-10-04 08:15:43 -07:00
Leonardo de Moura
bf01cfeec5
fix(frontends/lean): avoid superfluous local references of the form @-1 (@ f)
,
...
This kind of term also confuses the elaborator
2014-10-04 07:55:32 -07:00
Leonardo de Moura
e71d4548de
fix(frontends/lean): universe levels associated with section variables should not be fixed in the section
2014-10-04 07:13:19 -07:00
Leonardo de Moura
938e12baa1
feat(frontends/lean/notation_cmd): allow local numeric notation
2014-10-03 13:55:57 -07:00
Leonardo de Moura
fd013e8d07
chore(tests/lean/run/group3): cleanup test
2014-10-03 13:55:57 -07:00
Leonardo de Moura
c0725d1934
refactor(frontends/lean): remove 'including' expressions
2014-10-03 09:09:27 -07:00
Leonardo de Moura
01d4644026
fix(frontends/lean): bug in include/omit commands: in the end of section/context, the configuration must be restored
2014-10-03 08:52:35 -07:00
Leonardo de Moura
284f300440
feat(frontends/lean): add 'include' and 'omit' commands, closes #184
2014-10-03 07:23:24 -07:00
Leonardo de Moura
6950b4aa9b
fix(frontends/lean/decl_cmds): do not allow section parameters/variables to shadow existing parameters/variables
2014-10-02 18:29:41 -07:00
Leonardo de Moura
f006d93794
feat(frontends/lean): section variables occur after section parameters
2014-10-02 17:55:34 -07:00
Leonardo de Moura
0a13e7863a
feat(frontends/lean): enforce rule section parameters cannot depend on section variables
2014-10-02 17:55:34 -07:00
Leonardo de Moura
bf081ed431
refactor(kernel): rename var_decl to constant_assumption
...
Motivation: it matches the notation used to declare it.
2014-10-02 17:55:34 -07:00
Leonardo de Moura
4946f55290
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-02 17:55:34 -07:00
Leonardo de Moura
f78d831de3
refactor(frontends/lean): remove hardcoded Type', and define it using notation
2014-10-02 14:29:51 -07:00
Leonardo de Moura
4cb54ac825
feat(frontends/lean/elaborator): more strict test for bad universe solution
2014-10-02 14:29:51 -07:00
Leonardo de Moura
98e66586e9
feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit
2014-10-02 14:29:51 -07:00
Leonardo de Moura
153e3927ac
feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type.
2014-10-01 18:50:17 -07:00
Leonardo de Moura
e64d5c4a4a
refactor(library/data/nat): use new operator '!'
2014-10-01 18:39:47 -07:00
Leonardo de Moura
716cd4d651
refactor(library): rename namespace eq_ops to eq.ops
2014-10-01 17:51:17 -07:00
Leonardo de Moura
ead827d6b7
feat(frontends/lean): add !
operator the "dual" of @
, closes #220
2014-10-01 17:13:41 -07:00
Leonardo de Moura
bc6ebf34be
feat(library/data/bool): do not use !
as notation for bnot, rename band/bor -> and/or
2014-10-01 17:00:03 -07:00
Leonardo de Moura
c46ec6a548
fix(frontends/lean): missing type information for INFO, fixes #218
2014-10-01 14:29:07 -07:00
Leonardo de Moura
f863d82e69
fix(frontends/lean/pp): pp was not taking into account new namespace name resolution rules, fixes #216
2014-10-01 11:24:45 -07:00
Leonardo de Moura
966366e18e
feat(kernel/inductive): relaxed rules for defining datatypes with explicit universes, closes #217
2014-10-01 10:56:05 -07:00
Leonardo de Moura
263b081e69
fix(frontends/lean/inductive_cmd): temporary aliases must take explicit universes into account, fixes #215
2014-10-01 10:24:44 -07:00
Leonardo de Moura
2730e5163e
feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message
...
See new test for explanation.
2014-09-30 18:04:04 -07:00
Leonardo de Moura
113879a7dd
feat(frontends/lean/server): sort exact matches by size in FINDP
2014-09-29 16:44:55 -07:00
Leonardo de Moura
a0c37b231f
feat(kernel/expr): add hash_bi function that takes binder information into account
2014-09-29 16:44:55 -07:00
Leonardo de Moura
0d6d746d98
feat(frontends/lean): check modification time of imported files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-29 15:17:27 -07:00
Leonardo de Moura
21be308884
feat(frontends/lean/inductive_cmd): infer implicit argument annotation after elaboration, allow user to disable it by using '()' annotation, closes #210
2014-09-29 11:11:17 -07:00
Leonardo de Moura
9c55bbb871
feat(frontends/lean/elaborator): report an error when Type becomes a Prop after elaboration, closes #208
2014-09-29 08:18:10 -07:00
Leonardo de Moura
397395bbc9
feat(frontends/lean): allow user to associate priorities to class-instances, closes #180
2014-09-28 12:20:42 -07:00
Leonardo de Moura
22e47430b5
feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore
2014-09-27 21:50:39 -07:00
Leonardo de Moura
8e7aac1eb4
fix(frontends/lean): add 'eval' command
2014-09-26 20:16:03 -07:00
Leonardo de Moura
69f50adb2e
fix(frontends/lean/server): must save the starting environment/options when reprocessing file, fixes #209
2014-09-26 15:36:47 -07:00
Leonardo de Moura
a3e38dc8a0
feat(frontends/lean): allow users to define "numeral notation"
2014-09-26 14:55:23 -07:00
Leonardo de Moura
631ebc6c4b
fix(tests/lean/uni_bug1): make sure test does not produce a 'used sorry' warning.
...
Thus, the output behavior is the same when we compile lean with/without IGNORE_SORRY=ON
2014-09-26 09:42:31 -07:00
Leonardo de Moura
c775da16ec
feat(frontends/lean/elaborator): discard partial solution during
...
class-instance resolution, use only tactic_hints associated with
classes, enforce is_strict
2014-09-25 19:46:08 -07:00
Leonardo de Moura
10a4148adb
fix(tests): make sure tests can be executed on Windows msys2 shell
2014-09-20 15:51:24 -07:00
Leonardo de Moura
8fe7465ade
fix(frontends/lean/pp): when formatting a coercion to function-class
...
that contains implicit arguments
2014-09-20 09:56:46 -07:00
Leonardo de Moura
fd5daa8fda
feat(frontends/lean): use coercions to function-class and sort-class in
...
function arguments, closes #203
2014-09-20 09:00:10 -07:00
Leonardo de Moura
86f06a54ea
refactor(library/data/vector): rename 'vec' to 'vector'
2014-09-19 16:20:50 -07:00
Leonardo de Moura
4e2377ddfc
refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
5d8c7fbdf1
refactor(frontends/lean): replace '[private]' modifier with 'private
...
definition' and 'private theorem', '[private]' is not a hint.
2014-09-19 15:54:32 -07:00
Leonardo de Moura
08ccd58eb6
feat(frontends/lean): add 'reducible' modifier for controlling which
...
definitions are unfolded during elaboration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8
feat(frontends/lean): definitions are opaque by default
2014-09-19 15:54:32 -07:00
Leonardo de Moura
48dbd13eef
feat(frontends/lean): allow transient classes/instances, i.e.,
...
classes/instances that are not saved in .olean files
2014-09-19 15:54:32 -07:00
Leonardo de Moura
49d5af473d
refactor(kernel): remove support for proof irrelevant classes
...
Motivation: we can use Prop
2014-09-19 07:32:07 -07:00
Leonardo de Moura
dd31ed60b0
refactor(library): remove unnecessary file hott_kernel, HoTT and
...
standard library have been merged
2014-09-18 20:30:37 -07:00
Leonardo de Moura
b3e05a2fe9
refactor(frontends/lean/scanner): remove dependency to seekg and unget
...
methods
It is not safe to use seekg for textual files. Here is a fragment from a
C++ manual:
seekg() and seekp()
This pair of functions serve respectively to change the position of stream pointers get and put. Both functions are overloaded with two different prototypes:
seekg ( pos_type position );
seekp ( pos_type position );
Using this prototype the stream pointer is changed to an absolute position from the beginning of the file. The type required is the same as that returned by functions tellg and tellp.
seekg ( off_type offset, seekdir direction );
seekp ( off_type offset, seekdir direction );
Using this prototype, an offset from a concrete point determined by
parameter direction can be specified. It can be:
ios::beg offset specified from the beginning of the stream
ios::cur offset specified from the current position of the stream pointer
ios::end offset specified from the end of the stream
The values of both stream pointers get and put are counted in different
ways for text files than for binary files, since in text mode files some
modifications to the appearance of some special characters can
occur. For that reason it is advisable to use only the first prototype
of seekg and seekp with files opened in text mode and always use
non-modified values returned by tellg or tellp. With binary files, you
can freely use all the implementations for these functions. They should
not have any unexpected behavior.
2014-09-18 15:24:48 -07:00
Leonardo de Moura
243f80231a
chore(kernel): fix style and lua bindings
2014-09-17 18:30:28 -07:00
Leonardo de Moura
78ad24a697
feat(frontends/lean/server): add SYNC command, closes #199
2014-09-16 18:42:34 -07:00
Leonardo de Moura
e3e2370a38
feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-16 18:03:40 -07:00
Leonardo de Moura
50f788a427
fix(tests/lean/interactive): adjust test to library reorg
2014-09-16 13:16:46 -07:00
Jeremy Avigad
74cb289d48
refactor(library): rename algebra directory to struc, move categories.lean to algebra
2014-09-16 13:13:01 -07:00
Jeremy Avigad
9988914189
refactor(library/logic): move files in classes directory to core
2014-09-16 13:13:01 -07:00
Leonardo de Moura
dffe9a6f17
fix(frontends/lean/elaborator): more robust support for coercions to
...
function-class that contains implicit arguments
2014-09-16 13:08:34 -07:00
Leonardo de Moura
d0d23eb525
fix(frontends/lean/inductive_cmd): improve name resolution in inductive
...
command
The new test demonstrates the problem being fixed by this commit
2014-09-16 09:48:51 -07:00
Leonardo de Moura
851444b77a
test(tests/lean/interactive): test for issue #193
2014-09-15 16:07:23 -07:00
Leonardo de Moura
8e52c478b1
refactor(library/data/num): add 'succ', 'pred' and 'size' (aka number of bits),
...
rename is_inhabited theorems
2014-09-15 16:05:17 -07:00
Leonardo de Moura
af2c3b1815
fix(frontends/lean/info_manager): bug in save_environment_options,
...
server was displaying old results
2014-09-15 16:05:17 -07:00
Leonardo de Moura
edcbe6fe10
feat(frontends/lean): allow multiple coercions from class A to B, closes #187
...
See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-14 12:59:43 -07:00
Leonardo de Moura
029acbd1df
feat(library/coercion): better support for coercions to function-class. closes #185
2014-09-12 13:17:20 -07:00
Leonardo de Moura
a2e36e97f2
fix(frontends/lean/builtin_cmds): allow coercion command inside section, fixes #186
2014-09-12 12:13:29 -07:00
Leonardo de Moura
010ecebfea
feat(frontends/lean): add proof-qed expression
...
Remark: we still have to add support to it in the elaborator.
Right now, it is just an embellished parenthesis.
2014-09-11 18:14:49 -07:00
Leonardo de Moura
7ffe73b8ca
fix(frontends/lean): name clash inside section, fixes #181
2014-09-11 16:37:23 -07:00
Leonardo de Moura
5cff53c447
test(tests/lean/run): add section test
2014-09-11 15:33:20 -07:00
Leonardo de Moura
85f7132efe
feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes #175 , closes #173 , closes #68
2014-09-11 14:49:35 -07:00
Leonardo de Moura
b82092a123
fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172
2014-09-10 08:39:39 -07:00
Leonardo de Moura
570879b55f
feat(frontends/lean): add declaration to namespace without opening it, closes #161
2014-09-09 18:02:14 -07:00
Leonardo de Moura
efb14d906b
chore(tests/lean): add untracked tests
2014-09-09 16:21:30 -07:00
Leonardo de Moura
9b9adf8831
refactor(library): replace decidable_eq with abbreviation
2014-09-09 16:09:05 -07:00
Leonardo de Moura
47e02342bb
feat(frontends/lean/elaborator): use whnf in class-instance resolution, closes #160
2014-09-09 15:04:44 -07:00
Leonardo de Moura
abdd784729
feat(shell): start 'lean --server' with 'pp.beta = true'
2014-09-09 14:13:35 -07:00
Leonardo de Moura
ee196bbf1a
fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151
2014-09-09 12:49:32 -07:00
Leonardo de Moura
d8caa294b5
fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-09 11:02:54 -07:00
Leonardo de Moura
05c6e1461e
fix(tests/lean/interactive): interactive tests expected output, they must include the new '-- BEGINWAIT' messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-09 09:47:19 -07:00
Leonardo de Moura
187661aa6a
feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs
2014-09-09 09:27:26 -07:00
Leonardo de Moura
4088cdc139
chore(frontend/lean/pp_options): use consistent name convention for pp option names
2014-09-09 09:27:26 -07:00
Leonardo de Moura
b4793df653
feat(frontends/lean): rename '[fact]' to '[visible]'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-08 07:47:42 -07:00
Leonardo de Moura
559dd586f2
feat(library): add 'decidable_eq' class
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-07 22:23:36 -07:00
Leonardo de Moura
cbdfb0dcdc
feat(frontends/lean/elaborator): (Pi/forall) intro in class inference, closes #77
2014-09-07 19:59:34 -07:00
Leonardo de Moura
2631979f5c
fix(library/scoped_ext): section/context should not affect namespace
2014-09-07 19:59:34 -07:00
Leonardo de Moura
3310eb3dfc
feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-07 12:29:32 -07:00
Leonardo de Moura
5549295c47
fix(frontends/lean/inductive_cmd): bug when elaborating inductive tyoe parameters
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 11:38:32 -07:00
Leonardo de Moura
bbff564a1c
feat(frontends/lean): persistent notation in sections
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 11:14:20 -07:00
Leonardo de Moura
b5f595c432
fix(frontends/lean/inductive_cmd): bugs when declarating inductive datatypes in sections, fixes #141 , fixes #142
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 19:17:09 -07:00
Leonardo de Moura
9412e604c8
refactor(library/data): cleanup datatypes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 22:31:52 -07:00
Leonardo de Moura
6632a50015
refactor(library): add namespaces 'or', 'and' and 'iff'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 21:25:21 -07:00
Leonardo de Moura
68d9bef860
refactor(library): add 'eq' and 'ne' namespaces
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 18:41:06 -07:00
Leonardo de Moura
2bc6f92d33
refactor(library): add 'and' namespace
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:44:53 -07:00
Leonardo de Moura
364bba2129
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00
Leonardo de Moura
8743394627
refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
653141135d
chore(tests/lean): add missing tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
ffc871ea8c
feat(frontends/lean/server): only display 'EXTRA_TYPE' info when the column number is provided to the 'INFO' command, closes #133
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 14:02:53 -07:00
Leonardo de Moura
9d0a4d21d4
chore(tests/lean/interactive): adjust test expected output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 10:00:42 -07:00
Leonardo de Moura
f9a90b9920
feat(frontends/lean): add 'export' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 18:37:01 -07:00
Leonardo de Moura
5e18e6609c
feat(frontends/lean): add 'as' clause to 'open' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 17:37:02 -07:00
Leonardo de Moura
e51c4ad2e9
feat(frontends/lean): rename 'using' command to 'open'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 16:00:38 -07:00
Leonardo de Moura
e14814d4bf
feat(frontends/lean): add '[protected]' modifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 15:01:13 -07:00
Leonardo de Moura
2ca0a22e2c
fix(tests/lean/interactive/in4): adjust test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 01:35:46 -07:00
Leonardo de Moura
0f9478d91e
feat(frontends/lean): add 'class' command back
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 15:04:23 -07:00
Leonardo de Moura
8dec18018c
refactor(library/data/list): avoid placeholders '_', make first argument of false_elim implicit
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-01 19:44:04 -07:00
Leonardo de Moura
b7d7f12b8e
fix(frontends/lean/info_manager): several bugs: invalid flag was not being reset for empty lines, merge with overwrite=false was adding 'poluting' state, --NAY generation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-30 10:35:36 -07:00
Jeremy Avigad
6ffd719c1a
refactor(library/logic): move identities from classical to identities
2014-08-29 22:28:22 -07:00
Leonardo de Moura
59d3227eaa
fix(tests/lean/interactive): test output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 18:17:07 -07:00
Leonardo de Moura
9a4472cff5
fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 14:32:53 -07:00
Leonardo de Moura
b9489ce585
fix(frontends/let): let-expression pretty printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 10:58:27 -07:00
Leonardo de Moura
d8548369e7
feat(frontends/lean/pp): improve let-expr pretty printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 07:46:58 -07:00
Leonardo de Moura
be56fcf0bd
fix(frontends/lean/pp): pretty print 'let-expressions', closes #87
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 18:20:58 -07:00
Leonardo de Moura
1e80a9dfe9
feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 16:27:52 -07:00
Leonardo de Moura
d536475e49
refactor(library): more implicit_args for: and_assoc, and_comm, or_assoc, or_comm, if_pos, if_neg
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 11:10:04 -07:00
Leonardo de Moura
6b7e79b62f
feat(library/data/nat): mark more arguments implicit
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 10:38:58 -07:00
Leonardo de Moura
8de9cab62d
test(tests/lean/interactive): add --server test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 07:41:38 -07:00
Jeremy Avigad
00a049a667
refactor(library/logic): rename connectives -> core, basic -> connectives
2014-08-27 18:43:24 -07:00
Leonardo de Moura
2d78387541
refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 18:34:09 -07:00
Leonardo de Moura
477b7b4811
fix(tests/lean/run/class_coe): adjust test to reflect library changes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 17:55:42 -07:00
Leonardo de Moura
8719dff361
fix(frontends/lean): distribute '@' over choice
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 16:31:18 -07:00
Leonardo de Moura
c7e9e238ec
fix(frontends/lean/server): ignore output produced by worker thread, fixes #98
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 10:46:49 -07:00
Leonardo de Moura
a8d58fdd33
refactor(library): mark absurd_elim argument as implicit
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 18:27:39 -07:00
Leonardo de Moura
dd99e60a00
refactor(frontends/lean/info_manager): store environment+options in the info_manager, fixes #96
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 18:07:09 -07:00
Leonardo de Moura
40e4a1efa9
fix(tests/lua/slow): reduce test size to avoid stackoverflow on OSX when compiling without Boost
...
Signed-off-by: Leonardo de Moura <leodemoura@cmacslab5.modck.cs.cmu.edu>
2014-08-26 17:39:52 -04:00
Leonardo de Moura
4ab0dd4700
fix(tests/lean): adjust test to reflect recent changes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 09:12:18 -07:00
Leonardo de Moura
c11fd6b0d2
fix(tests/lean/run): adjust tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 21:39:46 -07:00
Leonardo de Moura
04d9eb17d1
feat(kernel/conveter): improve support for proof irrelevant in the converter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 11:19:18 -07:00
Leonardo de Moura
42a8fb5965
chore(tests/lean/run/matrix): simplify same_dim_irrel proof
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 09:27:19 -07:00
Leonardo de Moura
60d5e87a66
test(tests/lean/run): add matrix test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 09:04:39 -07:00
Leonardo de Moura
cbc81ea6c5
chore(*): minimize dependencies on tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 19:58:48 -07:00
Leonardo de Moura
dbaf81e16d
refactor(library): remove unnecessary 'standard' subdirectory
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Jeremy Avigad
47a1c00a6d
refactor(library/standard): collect notation in general_notation
2014-08-23 17:53:02 -07:00
Leonardo de Moura
2f699fa53a
feat(*): make sections 'permanent', and add 'transient' contexts, closes #88
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 15:45:15 -07:00
Leonardo de Moura
e602c4ba49
feat(frontends/lean): change multicomment to /- ... -/
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:55:13 -07:00
Leonardo de Moura
c5a44aca44
fix(frontends/lean/elaborator): do not expose type information produced when synthesizing class instances
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:07:12 -07:00
Leonardo de Moura
a5f0593df1
feat(*): change inductive datatype syntax
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:46:10 -07:00
Leonardo de Moura
626cd952e7
test(tests/lean/run): add overload test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:23:33 -07:00
Leonardo de Moura
01000ff7df
feat(library): add typed_expr macro
...
We use it to enforce that a let-variable has the expected type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 11:26:06 -07:00
Leonardo de Moura
937c465685
fix(library/unifier): too much reduction
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 21:37:51 -07:00
Leonardo de Moura
07bc0727e2
feat(frontends/lean): 'let [inline]' is the default
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 18:24:22 -07:00
Leonardo de Moura
6cf73b51e2
fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 17:56:18 -07:00
Leonardo de Moura
bb6dbe0e6f
fix(library/unifier): we should preprocess choice constraints before we start solving any constraint, fixes #85
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
725f5ba0a0
feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
359c72b02f
fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 09:28:07 -07:00
Leonardo de Moura
8375626cb6
fix(doc/lean/tutorial): adjust tutorial to library changes, fix test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 18:32:53 -07:00
Jeremy Avigad
6264fb52d6
fix(lean/library/standard): fix tests, more cleanup
2014-08-20 18:04:31 -07:00
Leonardo de Moura
f5987b7bda
refactor(library/unifier): make it easier to add new options to the unifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 17:30:08 -07:00
Leonardo de Moura
9588336c15
refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
b60c9d9ecc
test(tests/lean/run): add test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
f0d50e0d33
feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
08ae17650b
feat(frontends/lean): try overloaded notation and declarations in the order they were defined
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
919f02983e
feat(frontends/lean/elaborator): case-split on coercions that cannot be resolved by postponing
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
4a96fefd96
fix(library/unifier): bug in unifier priority queue
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
1d306c09ee
fix(tests/lean/interactive): remove leftover from test output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 17:29:52 -07:00
Leonardo de Moura
05b0f24cb5
fix(frontends/lean/decl_cmds): improve error message for invalid end of theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 17:03:54 -07:00
Leonardo de Moura
13af81d554
fix(tests/lean/interactive): adjust test output to reflect new features
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 15:23:53 -07:00
Leonardo de Moura
55b0a03e3d
refactor(frontends/lean/info_manager): to allow cache to be used when producing info data, fixes #37 , closes #45
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 12:16:32 -07:00
Leonardo de Moura
1436212a34
fix(library/unifier): use depth-first search strategy for solving class-instance constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-16 13:51:24 -07:00
Leonardo de Moura
670bfe24f5
chore(build): remove hott library directory, and move hott tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 13:30:56 -07:00
Leonardo de Moura
094459504b
fix(tests/lean/run): adjust test to changes in the library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 13:27:18 -07:00
Leonardo de Moura
28b7d87f1f
feat(frontends/lean/pp): pretty print numerals
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 09:12:22 -07:00
Leonardo de Moura
e778e3faec
fix(tests/lean): adjust tests expected output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-13 12:35:14 -07:00
Leonardo de Moura
60ab6d3bd8
feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
7d0c0818e5
test(tests/lean/slow): add self contained path_groupoids test file
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-11 16:44:30 -07:00
Leonardo de Moura
70c0eda9fc
feat(frontends/lean): make sure all scopes are closed in the end of the module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 17:08:59 -07:00
Leonardo de Moura
1a67e69678
feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:59:08 -07:00
Leonardo de Moura
2486c483cf
chore(kernel/error_msgs): change type mismatch error messages, closes #33
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:18:40 -07:00
Leonardo de Moura
9e6c5695be
fix(library/unifier): make sure the imitation step is type correct, fix ensure_sufficient_args
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:09:45 -07:00
Leonardo de Moura
4ad7e709aa
feat(frontends/lean): default for inductive types, closes #32
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 07:52:37 -07:00
Leonardo de Moura
8d9ca4c4ea
fix(tests/lean): remove obsolete test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 19:40:02 -07:00
Leonardo de Moura
a173b7f6e6
test(tests/lean/interactive): add old 'interactive' tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 14:57:08 -07:00
Leonardo de Moura
069f217215
fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 17:21:21 -07:00
Leonardo de Moura
9cc2015caa
feat(library/unifier): better error message for invalid local context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 16:25:22 -07:00
Leonardo de Moura
d1924097d5
feat(library/match): add 'local' backtracking
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 10:09:00 -07:00
Leonardo de Moura
e6ffda0c51
feat(library/match): add basic match_plugin that just invokes whnf before failing
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 08:37:03 -07:00
Leonardo de Moura
56d151ef7f
feat(frontends/lean): 'partial' aliases. closes #24
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 22:08:10 -07:00
Leonardo de Moura
c34c2f4f5c
feat(library/match): match universe levels
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 18:30:30 -07:00
Leonardo de Moura
0d5e346143
fix(library/expr_lt): make sure the builtin order is AC-compatible
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 15:51:10 -07:00
Leonardo de Moura
63d478c63f
fix(tests/lua/hop1): incorrect assertion
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 20:06:50 -07:00
Leonardo de Moura
552be37d48
feat(library/hop_match): port higher-order (pattern) matcher to Lean 0.2, we still have to implement support for universe levels
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 16:03:58 -07:00
Leonardo de Moura
50b0c17092
feat(library/unifier): add more information in error messages due to type errors when assigning metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 09:49:30 -07:00
Leonardo de Moura
938b4e8421
test(tests/lean/run): add unicode in identifiers test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 20:05:46 -07:00
Leonardo de Moura
fbc4a7af3b
feat(library/unifier): when unifier.expensive == true, then use only restrict higher-order unification (a fragment slightly more general than higher-order pattern matching) for solving class-instance constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 14:30:25 -07:00