lean2

Author	SHA1	Message	Date
Leonardo de Moura	0ffb7c080f	fix(tests/lean/run/inv_bug2): adjust test to reflect changes at data.vector	2015-01-08 12:11:52 -08:00
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	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	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	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	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	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	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	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
Leonardo de Moura	5e2185cfbe	feat(library/unifier): postpone as much as possible universe constraints of the form ?m1 =?= max(l1, l2) and ?m1 =?= imax(l1, l2) where ?m1 occurs in the right hand side. When there is nothing else to be done, try to solve them by reducing to ?m1 = l1 and ?m1 = l2. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-08-02 09:14:35 -07:00
Leonardo de Moura	3795d466c1	fix(frontends/lean/elaborator): provide type information for expressions using '@' operator, and strict function applications Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-08-01 20:57:24 -07:00
Leonardo de Moura	4cb8fb20fe	fix(frontends/lean/elaborator): bug when mixing string and non-strict implict arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-08-01 10:58:20 -07:00
Leonardo de Moura	01908c4dac	chore(tests/lean): add 'expensive' file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-08-01 10:35:32 -07:00
Leonardo de Moura	8e6324185a	fix(tests/lean): adjust tests to new library structure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-08-01 09:37:23 -07:00
Leonardo de Moura	6ca80b5000	feat(frontends/lean): add 'sorry' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-31 18:35:57 -07:00
Leonardo de Moura	de05c041c7	feat(library/unifier): add flag for enabling/disabling expensive extensions in the unifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-31 16:46:16 -07:00
Leonardo de Moura	f57fc33442	fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-31 16:46:16 -07:00
Leonardo de Moura	9637ceb86e	feat(frontends/lean): allow user to provide a terminator for 'foldr' and 'foldl' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-30 15:04:44 -07:00
Leonardo de Moura	450131692a	fix(library/converter): missing constraint on eta expansion Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-30 10:43:47 -07:00
Leonardo de Moura	936bb2744b	fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 17:32:55 -07:00
Leonardo de Moura	320bc55e85	fix(frontends/lean/elaborator): use preprocessed expression when displaying errors Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 14:25:50 -07:00
Leonardo de Moura	b15f1bb8c7	fix(frontends/lean/elaborator): apply coercions in definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 13:55:39 -07:00
Leonardo de Moura	501cae37e5	fix(frontends/lean/parser): bug in check_constant_next (when invoked inside of a section) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 13:04:58 -07:00
Leonardo de Moura	105c29b51e	refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-28 19:59:38 -07:00
Leonardo de Moura	5f360cd8ec	feat(kernel/error_msgs): improve application type mismatch error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-28 07:08:12 -07:00
Leonardo de Moura	4b2e403023	test(tests/lean/run): add more tests sent by Cody Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-27 12:17:38 -07:00
Leonardo de Moura	faee08591f	fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not. The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-27 12:12:54 -07:00
Leonardo de Moura	6ca120bf77	test(tests/lean/run): add Cody's file to test suite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-27 08:17:46 -07:00
Leonardo de Moura	0cdd4a267c	feat(frontends/lean/pp): pretty print 'show' expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 21:56:35 -07:00
Leonardo de Moura	60cc9ac8e2	feat(frontends/lean/pp): pretty print 'have' expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 21:35:26 -07:00
Leonardo de Moura	cf35c07786	fix(frontends/lean): fix 'let' annotation placement and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 21:00:22 -07:00
Leonardo de Moura	206206060f	test(tests/lean/hott): add some of Vladimir's definitions as tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 20:50:37 -07:00
Leonardo de Moura	70ef92cd5e	feat(build): add tests/lean/slow test directory, and add nat_wo_hints.lean file that elaborates nat.lean without using any hint Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 10:53:44 -07:00
Leonardo de Moura	23af5ab217	fix(library/unifier): eager whnf application Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 10:37:02 -07:00
Leonardo de Moura	709b5ce90f	fix(kernel/justification): duplicate position Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 21:16:49 -07:00
Leonardo de Moura	70c887a0bd	fix(library/unifier): fix cryptic error message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 21:10:32 -07:00
Leonardo de Moura	e79b0b11cf	test(tests/lean/run): another test for the unifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 20:55:05 -07:00
Leonardo de Moura	cf44c80ffb	fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 16:00:38 -07:00
Leonardo de Moura	7b84503133	fix(library/unifier): do not let a unification plugin to 'prioritize' a flex-flex constraint, and add missing case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 15:03:57 -07:00
Leonardo de Moura	0f12e5a35b	fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 13:49:45 -07:00
Leonardo de Moura	a59eec39b8	feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 09:44:40 -07:00
Leonardo de Moura	21176c61fe	fix(tests/lean): move crash.lean to different directory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 08:48:35 -07:00
Leonardo de Moura	e7c7d5718a	fix(frontends/lean/pp): fix bug in the pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 08:30:30 -07:00
Leonardo de Moura	15c1e39f88	feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-24 23:43:40 -07:00
Leonardo de Moura	905a1095f9	fix(tests/lean/run/tactic14): remove not_intro, it is not needed anymore Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-24 23:41:23 -07:00
Leonardo de Moura	5529ef1056	feat(library/standard): add function 'helper' module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-24 16:29:39 -07:00
Leonardo de Moura	d998bf9300	test(tests/lean/run): add some 'lost' tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-23 08:22:53 -07:00
Leonardo de Moura	b522ea6f2d	refactor(library/standard): rename bit to bool Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-22 09:49:54 -07:00
Leonardo de Moura	5eaf04518b	refactor(*): rename Bool to Prop Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-22 09:43:18 -07:00
Leonardo de Moura	a9f7d87aae	test(tests/lean/run/decidable): show implicit argument that is computed automatically Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-22 05:58:36 -07:00
Leonardo de Moura	5e8c128b00	feat(library/standard): add more decidable instances Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-20 01:10:49 +01:00
Leonardo de Moura	6b60db7b93	fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-19 09:55:34 +01:00
Leonardo de Moura	0f44e3c9f4	fix(frontends/lean): calc configuration commands, add check_constant_next auxiliary method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-15 01:19:47 +01:00
Leonardo de Moura	2e6184a721	fix(frontends/lean): more bugs in section management Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-14 06:27:36 +01:00
Leonardo de Moura	8167ad329f	fix(frontends/lean): bug in section management Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-14 05:04:01 +01:00
Leonardo de Moura	fab7934265	refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-14 02:53:02 +01:00
Leonardo de Moura	e432e23115	test(tests/lean/run/class5): improve test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-13 22:39:16 +01:00
Leonardo de Moura	1d273fcfdd	chore(frontends/lean): rename 'obtains' to 'obtain' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-12 06:35:24 +01:00
Leonardo de Moura	1230e942aa	feat(library/unifier): handle 'first-order' flex-flex constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-11 04:51:28 +01:00
Leonardo de Moura	cf34f75ab5	feat(frontends/lean): add 'obtains' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-11 04:08:51 +01:00
Leonardo de Moura	6000270d35	chore(tests/lean): reactivate config.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 23:32:23 +01:00
Leonardo de Moura	e9c17b154c	fix(tests/lean): define LEAN_PATH in tests scripts Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 23:26:55 +01:00
Leonardo de Moura	92bb046854	test(tests/lean/run): add nested let-expr test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 15:56:15 +01:00
Leonardo de Moura	c13c75b93e	feat(frontends/lean/pp): add option for displaying fully qualified names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 15:55:19 +01:00
Leonardo de Moura	06beff327f	test(tests/lean/run): add more universe tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 14:43:55 +01:00
Leonardo de Moura	49bc3fffbd	fix(frontends/lean/pp): purify procedure for local names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 14:13:51 +01:00
Leonardo de Moura	fc8ddcb0ce	feat(frontends/lean): improve 'check' command when used inside sections Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 14:07:41 +01:00
Leonardo de Moura	1a6d0784f2	feat(kernel/level): improve universe level normalization procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 13:49:41 +01:00
Leonardo de Moura	d9b2801eeb	feat(frontends/lean): use the same universe in declarations such as (A B : Type) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 13:18:52 +01:00
Leonardo de Moura	12d89ea0b9	fix(kernel/level): is_geq predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 13:18:41 +01:00
Leonardo de Moura	aff766430d	fix(frontends/lean/pp): universe pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-09 19:17:28 -07:00
Leonardo de Moura	43eba857cb	feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-09 18:47:10 -07:00
Leonardo de Moura	2ef7b9be2f	feat(frontends/lean): add basic pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-09 01:12:36 -07:00
Leonardo de Moura	2ad1a93657	test(tests/lean/run): add append tactic test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-08 18:21:22 -07:00
Leonardo de Moura	a1601e7a5f	feat(library/tactic/apply_tactic): add option for 'refreshing' universe metavariables in the 'apply' tactic The new test ../../tests/lean/run/tactic27.lean demonstrates why we need this feature. The tactic 'apply @refl' is actually 'apply @refl.{?l}'. It is used inside of a repeat tactical. Each iteration of the 'repeat' may need to use a different value for ?l. Before this commit, there was not way to say we want a fresh ?l each iteration. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-08 16:55:23 -07:00
Leonardo de Moura	4505016154	feat(frontends/lean): allow tactic_hints to be applied when class-instance mechanism fails Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-08 15:08:13 -07:00
Leonardo de Moura	5e836092cc	feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-08 15:08:13 -07:00
Leonardo de Moura	a3be63af73	feat(frontends/lean): add tactic_hint command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-08 15:08:13 -07:00
Leonardo de Moura	da4c1922e3	feat(frontends/lean): add '_root_' prefix for referencing names in the root namespace Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 19:15:46 -07:00
Leonardo de Moura	b43fb7448c	feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 19:00:06 -07:00
Leonardo de Moura	e6d4c01b88	feat(frontends/lean): check whether namespace exists or not in the 'using' command, add to_valid_namespace_name helper function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 18:17:10 -07:00
Leonardo de Moura	bd1873f6b1	feat(frontends/lean): add coercion modifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 17:48:20 -07:00
Leonardo de Moura	08465f049a	feat(frontends/lean): remove [class] annotation and 'class' command, they are redundant, we only need [instance] and 'instance' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 16:09:30 -07:00
Leonardo de Moura	112353861c	feat(frontends/lean): rename command 'reset_proof_qed' to 'set_proof_qed' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 15:48:16 -07:00
Leonardo de Moura	c16951aba6	fix(library/aliases): aliasing behavior The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 15:40:55 -07:00
Leonardo de Moura	b9d08ff28c	feat(frontends/lean/builtin_cmds): allow many namespaces in the same 'using' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 14:53:06 -07:00
Leonardo de Moura	d30f387e72	feat(library/standard): add namespace 'pair' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 14:48:19 -07:00
Leonardo de Moura	10b0dfeb37	feat(frontends/lean/class): allow many instances to provided with a single 'instance' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 14:41:14 -07:00
Leonardo de Moura	6ceecf6a15	feat(library/aliases): remove duplicates from aliasing tables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 12:59:57 -07:00
Leonardo de Moura	b956ce68d2	feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 12:50:43 -07:00
Leonardo de Moura	831de22bcd	fix(frontends/lean): bugs in notation management Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 09:31:42 -07:00
Leonardo de Moura	e8bd267a00	fet(frontends/lean): allow coercions to sort-class in the types of variable and definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-06 21:54:16 -07:00
Leonardo de Moura	48b28ad75c	fix(library/unifier): missing test in flex_rigid Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-06 21:36:23 -07:00
Leonardo de Moura	dcf7cf00ff	fix(*): bugs in the type checker, inductive datatypes, and unifier The bugs were indentified when performing the tiny change in the file tests/lean/run/group.lean	2014-07-06 18:44:56 -07:00
Leonardo de Moura	9a13bef4f3	fix(frontends/lean): fix (and simplify) parameter universe inference Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-06 16:56:54 -07:00
Leonardo de Moura	8e5ac54ae1	test(tests/lean/run): group experiments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 22:31:57 -07:00
Leonardo de Moura	55894f01e3	feat(frontends/lean): add 'opaque_hint' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 18:58:20 -07:00
Leonardo de Moura	e68a3e5251	test(tests/lean/run): add another class-instance example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 17:41:08 -07:00
Leonardo de Moura	59755289e4	feat(library/unifier): case split on constraints of the form (f ...) =?= (f ...), where f can be unfolded, and there are metavariables in the arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 15:52:40 -07:00
Leonardo de Moura	a52c9f4e2b	feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 09:43:16 -07:00
Leonardo de Moura	efabd2280c	feat(library/unifier): allow unifier to unfold opaque definitions of the current module It is not clear whether this is a good idea or not. In some cases, it seems to do more harm than good. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 00:46:03 -07:00
Leonardo de Moura	99fb6431a6	fix(frontends/lean/elaborator): support for local instances Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-04 18:38:08 -07:00
Leonardo de Moura	8ab0b5bee3	feat(frontends/lean/elaborator): use local declarations as class instances Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-04 18:18:25 -07:00
Leonardo de Moura	00e1a7db23	feat(frontends/lean/elaborator): add class instance elaboration Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-04 15:45:50 -07:00
Leonardo de Moura	b94ce412ae	fix(library/unifier): non-termination Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-04 10:32:01 -07:00
Leonardo de Moura	a97f82be1a	fix(library/standard): orelse notation, avoid conflict with inductive datatype declaration Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-04 10:10:05 -07:00
Leonardo de Moura	e0501104e2	feat(library/tactic): add 'fixpoint' tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-04 01:30:28 -07:00
Leonardo de Moura	7fb2b0f6d8	feat(kernel): add method 'may_reduce_later' to normalizer_extension, and improve unifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 22:31:05 -07:00
Leonardo de Moura	855ffcba34	feat(library/standard): add pairs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 20:43:16 -07:00
Leonardo de Moura	110b622b83	feat(library/unifier): add support for unification constraints of the form "(elim ... (?m ...)) =?= t", where elim is an eliminator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 20:41:51 -07:00
Leonardo de Moura	b5f63e78ca	feat(frontends/lean/notation_cmd): reuse existing precedence to increase compatibility with existing notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 17:23:29 -07:00
Leonardo de Moura	fa1857e6a9	fix(frontends/lean/notation_cmd): fix default, add 'prev' action Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 16:44:44 -07:00
Leonardo de Moura	abbd054b51	feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 13:04:46 -07:00
Leonardo de Moura	d63ccbcf94	fix(library/unifier): missing case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 10:51:59 -07:00
Leonardo de Moura	0ff145e59b	feat(library/tactic): add apply tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 09:20:01 -07:00
Leonardo de Moura	c1538bfc40	test(tests/lean/run): add 'apply subst' test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 09:07:56 -07:00
Leonardo de Moura	a7d660f875	feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 20:45:10 -07:00
Leonardo de Moura	5527955ba8	feat(frontends/lean): add 'proof-qed' notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 19:30:48 -07:00
Leonardo de Moura	60c637fb9d	feat(library/tactic): add 'exact' tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 18:37:32 -07:00
Leonardo de Moura	37b5b7c4c2	feat(library/tactic): rename 'exact' to 'assumption', 'exact' is a different tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 18:10:42 -07:00
Leonardo de Moura	ee531ec0e2	feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact] Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 14:09:01 -07:00
Leonardo de Moura	0f27856e4a	feat(library/tactic): new apply tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 13:14:50 -07:00
Leonardo de Moura	6ab46396d8	feat(library/tactic): expose 'trace' tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 10:52:45 -07:00
Leonardo de Moura	e1d909455c	refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 10:45:09 -07:00
Leonardo de Moura	a66a08c89e	feat(frontends/lean): parse strings as expressions of type 'string.string' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 10:00:55 -07:00
Leonardo de Moura	0198dfc7c5	feat(frontends/lean): parse numerals as expressions of type 'num.num' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 08:09:33 -07:00
Leonardo de Moura	7593ee1468	refactor(library/standard): remove parameter from 'tactic' inductive type Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-02 08:09:24 -07:00
Leonardo de Moura	b2b76b078f	feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-01 20:43:53 -07:00
Leonardo de Moura	5b69f88664	feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-01 16:55:41 -07:00
Leonardo de Moura	8d584e54da	feat(frontends/lean): add exact_apply Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-30 00:51:11 -07:00
Leonardo de Moura	33cb9382aa	feat(frontends/lean): add beta-reduction tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 19:41:54 -07:00
Leonardo de Moura	360e9b9486	feat(library/tactic): add apply tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 18:33:53 -07:00
Leonardo de Moura	6645fdeae0	feat(frontends/lean): add repeat tactic command, refactor tactic sequence notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 12:24:13 -07:00
Leonardo de Moura	2510d5722a	feat(frontends/lean): add unfold tactic command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 12:05:45 -07:00
Leonardo de Moura	6d09d82a7c	feat(frontends/lean): add notation for orelse tactic, add show and now tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 11:39:18 -07:00
Leonardo de Moura	a1bbb09de4	feat(frontends/lean): add notation for then tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 11:24:56 -07:00
Leonardo de Moura	ffa175009b	feat(frontends/lean): use tactics for solving unassigned metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:50:16 -07:00
Leonardo de Moura	1e39a21823	feat(frontends/lean): add basic tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:03:51 -07:00
Leonardo de Moura	7d5522e36a	chore(tests): add missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:03:51 -07:00
Leonardo de Moura	f5f3816596	chore(tests): cleanup test scripts Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:03:39 -07:00
Leonardo de Moura	cf28981f45	feat(tests/lean/run): add test_single script that sets the LEAN_PATH Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 07:47:46 -07:00
Leonardo de Moura	193ce35419	refactor(frontends/lean/inductive_cmd): redesign inductive datatype elaboration, use the new elaborator, and use simpler algorithm to infer the resulting universe Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 15:33:56 -07:00
Leonardo de Moura	0adacb5191	feat(kernel): add infer implicit, and use it to infer implicit arguments of inductive datatype eliminators, and tag whether parameters should be implicit or not in introduction rules in the module inductive_cmd Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 13:57:36 -07:00
Leonardo de Moura	47ff300d1a	fix(frontends/lean): '@' explicit mark Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-28 07:30:36 -07:00
Leonardo de Moura	ccce9d90a4	feat(frontends/lean/elaborator): add 'delayed coercions', add example demonstrating why the new feature is useful Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 18:39:23 -07:00
Leonardo de Moura	340dc622c6	fix(kernel/formatter): make sure simple formatter output is not sensitive to internal names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 14:58:59 -07:00
Leonardo de Moura	150d285b39	fix (library/unifier): occurs_context_check Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 14:45:36 -07:00
Leonardo de Moura	16bdc51fc4	refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 13:36:31 -07:00
Leonardo de Moura	a70f8dd98e	feat(kernel/inductive): mark parameters, type formers and indices as implicit parameters in the elimination rule Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 11:05:14 -07:00
Leonardo de Moura	5e0e737213	feat(library/scoped_ext): do not import 'children' namespace objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 10:32:34 -07:00
Leonardo de Moura	a7623845f9	test(tests/lean/run): add another example on how to deal with ambiguity Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 10:18:35 -07:00
Leonardo de Moura	930960c54d	fix(frontends/lean/builtin_cmds): abstract section parameters in the 'check' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 10:06:50 -07:00
Leonardo de Moura	cc21bfd01d	test(tests/lean/run): more tests on how to deal with ambiguity Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 09:32:26 -07:00
Leonardo de Moura	dc5553ea5c	test(tests/lean/run): add test demonstrating how to control ambiguity Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 09:32:19 -07:00
Leonardo de Moura	da6e92787a	test(tests/lean/run): add simple overloading test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 09:32:12 -07:00
Leonardo de Moura	acf8c13619	feat(kernel): add strict implicit arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 17:50:49 -07:00
Leonardo de Moura	4bc1f3cf81	test(lean/run): add elaborator tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 16:15:01 -07:00
Leonardo de Moura	49a6048060	test(lean/run): add another test for new elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 13:18:32 -07:00
Leonardo de Moura	3e7dfa6212	fix(frontends/lean): infer type of definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 08:39:14 -07:00
Leonardo de Moura	d055c4880f	feat(frontends/lean): connect new elaborator to frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 08:31:00 -07:00
Leonardo de Moura	603dafbaf7	refactor(kernel): remove 'let'-expressions We simulate it in the following way: 1- An opaque 'let'-expressions (let x : t := v in b) is encoded as ((fun (x : t), b) v) We also use a macro (let-macro) to mark this pattern. Thus, the pretty-printer knows how to display it correctly. 2- Transparent 'let'-expressions are eagerly expanded by the parser. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-24 16:27:27 -07:00
Leonardo de Moura	aa8b5655dd	feat(frontends/lean): add notation overwrite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-23 16:10:36 -07:00
Leonardo de Moura	5bd86754af	feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-22 17:51:00 -07:00
Leonardo de Moura	2589d60bfd	feat(frontends/lean): add nameless 'have' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 17:18:18 -07:00
Leonardo de Moura	4b227409bf	feat(frontends/lean): add 'then have' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 14:27:21 -07:00
Leonardo de Moura	4560413a92	feat(frontends/lean): add '[fact]' modifier for 'have' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 11:58:05 -07:00
Leonardo de Moura	39177ec10a	feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-20 11:58:05 -07:00
Leonardo de Moura	bdab979e09	feat(frontends/lean): add inductive_cmd Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 16:00:59 -07:00
Leonardo de Moura	3bb53810c5	test(lean/run): add notation test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 09:48:47 -07:00
Leonardo de Moura	08845be2fc	feat(frontends/lean/notation_cmd): improve 'notation' cmd Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 09:28:01 -07:00
Leonardo de Moura	3e3c4ee5ed	feat(frontends/lean/parser): add local_scope object to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 08:38:23 -07:00
Leonardo de Moura	6259d20218	feat(frontends/lean/parser): expand Lua parser API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 08:03:17 -07:00
Leonardo de Moura	813e033f54	test(lean): add simple example of notation implemented using Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 22:37:22 -07:00
Leonardo de Moura	4cbc429192	feat(frontends/lean/calc): add parse_calc function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 17:16:15 -07:00
Leonardo de Moura	e178979061	feat(frontends/lean): add calc_subst, calc_refl, calc_trans commands for configuring calc-expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 13:35:31 -07:00
Leonardo de Moura	819c8276f2	feat(frontends/lean/builtin_cmds): add 'variables' command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 08:25:00 -07:00
Leonardo de Moura	ea49176043	feat(frontends/lean/builtin_cmds): add 'using' command, and 'hiding/renaming' directives Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 18:42:39 -07:00
Leonardo de Moura	639d58f4c7	feat(frontends/lean/builtin_cmds): add 'print options' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 17:31:28 -07:00
Leonardo de Moura	3e377a9732	feat(frontends/lean/builtin_cmds): add 'set_option' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 17:27:43 -07:00
Leonardo de Moura	4f3da90443	feat(frontends/lean/builtin_exprs): add 'have' and 'show' expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 15:04:29 -07:00
Leonardo de Moura	873a5c8605	test(lean): add 'let' expression test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 14:11:26 -07:00
Leonardo de Moura	21c54755a9	fix(kernel/converter): bug in is_def_eq Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 14:09:12 -07:00
Leonardo de Moura	f70b1b028a	feat(frontends/lean): provide position to parse_fn external function, add 'by' expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 12:28:58 -07:00
Leonardo de Moura	34dfacc10e	refactor(frontends/lean): Bool does not need to be a reserved keyword Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 10:52:12 -07:00
Leonardo de Moura	6db265e7ab	feat(frontends/lean/builtin_exprs): parse '_' placeholder Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 10:41:08 -07:00
Leonardo de Moura	5ce0502a36	feat(frontends/lean/builtin_exprs): add parser for 'let' expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 09:50:34 -07:00
Leonardo de Moura	27130c9499	feat(frontends/lean): local notation 'shadows' global one Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 11:50:41 -07:00
Leonardo de Moura	28047a33ae	feat(frontends/lean): add local notation support Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 11:30:52 -07:00
Leonardo de Moura	64cafd6875	feat(frontends/lean/notation_cmd): add 'notation' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 10:49:05 -07:00
Leonardo de Moura	9b389a96d5	feat(frontends/lean/notation_cmd): modify infixl/infixr/postfix command syntax Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-15 08:28:49 -07:00
Leonardo de Moura	e7019ec840	feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 22:13:25 -07:00
Leonardo de Moura	891a3fb48b	feat(frontends/lean): add command block reader with snapshot and resume Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 14:13:32 -07:00
Leonardo de Moura	5fee6fd140	feat(shell/lean): add '-o' command line option Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 08:10:43 -07:00
Leonardo de Moura	282a35bd1b	feat(frontends/lean): add '#setline' directive Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-14 07:28:56 -07:00
Leonardo de Moura	fad4780d72	test(lean/run): add overload test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 18:06:44 -07:00
Leonardo de Moura	48c58af9b5	feat(frontends/lean/parser): allow explicit universe level to be provided to aliases and locals Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 18:00:52 -07:00
Leonardo de Moura	a65c43c0db	feat(frontends/lean/builtin_cmds): add definition command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 17:30:35 -07:00
Leonardo de Moura	01cecb76db	feat(frontends/lean/builtin_cmds): add 'variable' command family Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 15:13:50 -07:00
Leonardo de Moura	ce259e6265	feat(frontends/lean/parser): add namespace/section/end commands, add support for explicit universe levels, fix Type notation' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 11:34:43 -07:00
Leonardo de Moura	3bde699fbe	feat(frontends/lean/parser): add parse_level Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-12 12:34:55 -07:00
Leonardo de Moura	cffbae3667	test(tests/lean/run): add new test group, where we just execute Lean (and don't check output) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 21:07:23 -07:00
Leonardo de Moura	05edbe00ad	chore(shell): re-activate .lean tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 14:36:42 -07:00
Leonardo de Moura	1972a09021	feat(frontends/lean/builtin_cmds): add simple 'print' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 14:35:34 -07:00
Leonardo de Moura	2e8ebb6d9e	feat(frontends/lean/parser): add 'parse_commands' and 'parse_script' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-11 14:32:07 -07:00
Leonardo de Moura	3a0861bca7	test(lean): remove old test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 10:42:10 -07:00
Leonardo de Moura	9f06cd553e	test(lean): remove tests using Lean old syntax and kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 10:38:53 -07:00
Leonardo de Moura	e9dada5e14	refactor(builtin/kernel): use standard definition for 'or' and 'and' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-17 12:05:34 -08:00
Leonardo de Moura	1739b5c153	fix(kernel/type_checker): caching bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-12 10:43:01 -08:00
Leonardo de Moura	368fcb5ff9	refactor(builtin/kernel): rename refute to by_contradiction Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-12 08:49:19 -08:00
Leonardo de Moura	b7b868de85	fix(library/elaborator): bug reported by Jeremy Avigad Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-10 14:01:22 -08:00
Leonardo de Moura	a2d2e36f04	refactor(frontends/lean): remove notation for creating tuples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-10 09:03:42 -08:00
Leonardo de Moura	4317f67bd2	fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 18:57:33 -08:00
Leonardo de Moura	c45c1748d8	refactor(builtin/kernel): reorder congr1 arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 16:15:44 -08:00
Leonardo de Moura	8df7c7b02d	feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker We should not rely on this feature. It can be quite expensive. We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as is_convertible(num, Nat) If is_convertible starts unfolding opaque definitions, we would keep expanding num. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 11:31:24 -08:00
Leonardo de Moura	1ec01f5757	refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 16:04:44 -08:00
Leonardo de Moura	ad7b13104f	feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 15:03:16 -08:00
Leonardo de Moura	d4b08fcf96	feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx \|- ?m[inst:i v] == T and ctx \|- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 21:08:00 -08:00
Leonardo de Moura	593f1f2ebd	fix(frontends/lean): allow user set constants defined in other namespaces as opaque Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -08:00
Leonardo de Moura	363c4dc5c2	feat(library/elaborator): improve support for dependent pairs in the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -08:00
Leonardo de Moura	ea06bb2885	feat(frontends/lean/pp): change how lift local entries are pretty printed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:26:38 -08:00

... 12 13 14 15 16 ...

1714 commits