Leonardo de Moura
e4f0f6a9b4
feat(library): numeral normalization skeleton
2015-10-08 12:49:12 -07:00
Leonardo de Moura
1c4dea9941
fix(tests/lean): adjust tests to reflect changes in the pretty printer
2015-09-30 17:42:07 -07:00
Leonardo de Moura
542a998f0e
fix(tests/lean): adjust tests to reflect changes in the HoTT library
2015-09-25 09:46:51 -07:00
Leonardo de Moura
28a5ca5809
fix(frontends/lean): fixes #830
2015-09-18 07:51:02 -07:00
Leonardo de Moura
68dc39c106
fix(tests/lean/run/rewriter12): broken test, now ^[ is a token
2015-09-16 08:37:43 -07:00
Leonardo de Moura
df3100d2cd
fix(library/local_context): bug in abstract_locals procedure
2015-09-12 17:17:13 -07:00
Leonardo de Moura
1fdbd681cc
feat(frontends/lean/builtin_exprs): name hypothesis in suffices
...
closes #817
2015-09-03 16:09:39 -07:00
Leonardo de Moura
1dc1574ad4
fix(frontends/lean/parse_table): do not add 'no_info' annotation in tactic expressions
2015-09-02 20:51:06 -07:00
Leonardo de Moura
634c0b5e9d
feat(library/tactic,frontends/lean): propagate new options back to elaborator
2015-09-02 20:34:14 -07:00
Leonardo de Moura
44c6e92a64
fix(tests/lean): notation ℕ is now defined in the top-level
2015-09-01 14:58:14 -07:00
Leonardo de Moura
c84e886c7b
fix(frontends/lean/notation_cmd): fixes #808
...
This commit and 2b1d2c fixes #808
2015-08-31 18:05:58 -10:00
Leonardo de Moura
08169c5ac2
fix(library/unifier): fixes #809
...
Daniel is correct when he says the interaction between choice
case-splits, delta case-splits, and coercions can be subtle.
I believe the following condition
https://github.com/leanprover/lean/blob/master/src/frontends/lean/elaborator.cpp#L111
reduces counter-intuitive behavior. Example, the coercion should not
influence the resulting type.
BTW, by removing this condition, many files in the library broke when I
tried to compile from scratch
make clean-olean
make
I used the following workaround. Given a delta-delta constraint
f a =?= f b
If the terms are types, and no case-split will be performed, then
the delta-delta constraint is eagerly solved.
In principle, we don't need the condition that the terms are types.
However, many files break if we remove it. The problem is that many files in the standard
library are abusing the higher-order unification procedure. The
elaboration problems are quite tricky to solve.
I use the extra condition "the terms are types" because usually if they
are, "f" is morally injective, and we don't really want to unfold it.
Note that the following two cases do not work
check '{1, 2, 3}
check insert 1 (insert 2 (insert 3 empty))
Well, they work if we the num namespace is open, and they are
interpreted as having type (finset num)
2015-08-31 17:59:30 -10:00
Leonardo de Moura
2b1d2c21ad
fix(frontends/lean/util): bug when parsing priorities and numerals are overloaded
2015-08-31 15:08:21 -10:00
Leonardo de Moura
a3c404ac3b
feat(library/tactic/apply_tactic): do not report elaboration failure in apply tactic when proof_state.report_failure() is false
2015-08-21 15:45:52 -07:00
Leonardo de Moura
87349dc355
feat(frontends/lean/token_table): add 'proposition' keyword
2015-08-19 08:05:31 -07:00
Leonardo de Moura
3a72cd9621
fix(frontends/lean): rename multiword keyword "suffices to show" to "suffices"
2015-08-18 17:57:53 -07:00
Leonardo de Moura
3ce8c5d6f7
feat(frontends/lean): add "suffices to show A, from B, C" construct
2015-08-18 17:04:38 -07:00
Leonardo de Moura
9fcf3d4675
fix(tests/lean/extra): discrepancy between tests output when compiling Lean with IGNORE_SORRY
2015-08-18 12:42:22 -07:00
Leonardo de Moura
21c41f50ea
fix(frontends/lean/elaborator): fixes #803
2015-08-17 14:56:41 -07:00
Leonardo de Moura
b07a364d2f
feat(frontends/lean/parser): process multiple parsing actions
...
closes #800
2015-08-17 09:42:10 -07:00
Leonardo de Moura
b0dbc31d4b
test(tests/lean/list_vect_numerals): add test mixing nat,int,real,list,vector
2015-08-16 18:54:14 -07:00
Leonardo de Moura
ea04414058
feat(frontends/lean): allow user to overload notation containing foldr/foldl and/or scoped expressions
...
see new tests for a summary of new features
see issue #800
2015-08-16 18:24:30 -07:00
Leonardo de Moura
eb8f586dba
fix(library/normalize): fixes #801
2015-08-16 14:22:02 -07:00
Leonardo de Moura
6c934229f7
feat(kernel,library/module): only module reader can add declarations without type-checking them
2015-08-14 18:37:17 -07:00
Leonardo de Moura
5a6a4b45c1
fix(library/definitional/equations): fixes #796
2015-08-14 14:39:23 -07:00
Leonardo de Moura
d2eb99bf11
refactor(library/logic): move logic/choice.lean to init/classical.lean
...
choice axiom is now in the classical namespace.
2015-08-12 18:37:33 -07:00
Leonardo de Moura
cb9830beaf
refactor(library/logic/choice): move prop_decidable instance into namespace 'classical'
2015-08-12 17:06:15 -07:00
Leonardo de Moura
b4024982a2
refactor(library/data): move vector as indexed family to examples folder
2015-08-12 15:05:14 -07:00
Leonardo de Moura
602626803b
fix(frontends/lean/builtin_cmds): 'print axioms' and theorem queue
2015-08-11 21:08:45 -07:00
Leonardo de Moura
5d8d226640
fix(frontends/lean/parser): add support for decimals
...
Decimal numbers are notation for rationals.
If rat.of_num is not available, then an error is generated.
closes #793
2015-08-11 18:44:48 -07:00
Leonardo de Moura
66a59d5b51
feat(frontends/lean/util): remove hack that overrides priority namespace
...
closes #789
2015-08-11 18:01:40 -07:00
Leonardo de Moura
0b8f57841a
feat(frontends/lean/decl_cmds): closes #791
2015-08-11 17:53:33 -07:00
Jeremy Avigad
305f72bf4f
fix(tests/lean): fix three tests broken by setext renaming
2015-08-09 22:14:25 -04:00
Leonardo de Moura
582dbecfd0
feat(library,hott): add notation T1 : T2 as syntax sugar for (focus (T1; all_goals T2))
...
closes #775
2015-08-08 10:16:25 -07:00
Leonardo de Moura
1f34c72192
fix(frontends/lean/parser): fixes #770
2015-08-08 09:48:31 -07:00
Leonardo de Moura
dc2e702373
feat(library/unifier): generate approximate solution for universe constraints of the form (max u ?m =?= max u v)
...
closes #777
2015-08-08 09:29:59 -07:00
Leonardo de Moura
6c5832a564
feat(frontends/lean/decl_cmds): allow recursive examples
...
closes #774
2015-08-08 08:26:25 -07:00
Leonardo de Moura
06f20694c8
fix(frontends/lean/builtin_exprs): fixes #768
2015-08-08 04:20:17 -07:00
Leonardo de Moura
d46dbce86e
feat(library/tactic/tactic): apply substitution in 'then' combinator
...
closes #778
2015-08-08 03:42:21 -07:00
Floris van Doorn
7f76d7e648
fix(tests): update test
2015-08-07 13:34:41 -07:00
Leonardo de Moura
5568085ab9
fix(frontends/lean/elaborator): closes #771
...
Produce nicer error message when type/goal is a metavariable and
universe metavariables have already been instantiated with universe
parameters.
2015-08-07 13:29:22 -07:00
Leonardo de Moura
6a079fdd2d
fix(library/tactic/exact_tactic): fixes #779
2015-08-07 13:29:22 -07:00
Leonardo de Moura
f21647899f
feat(frontends/lean/builtin_exprs): rename 'show' hidden name to 'this'
...
This is useful if 'show' is recursive
2015-08-07 13:29:21 -07:00
Floris van Doorn
11b1f416f6
feat(nat): add unfold attributes to add, mul, sub and of_num in namespace nat_esimp in both libraries
2015-08-04 13:23:20 +02:00
Floris van Doorn
7a780b1b60
feat(hott): various minor changes in the HoTT library
2015-08-04 13:01:11 +02:00
Leonardo de Moura
0309a1e131
fix(tests/lean/extra/show_goal_bag): adjust test to recent changes in the standard library
2015-08-04 06:52:20 +02:00
Leonardo de Moura
1f304ad4b9
fix(frontends/lean/pp): pretty printing 'binder'
...
This commit also replaces many occurrences of 'binders' with 'binder'.
2015-07-31 11:27:38 -07:00
Leonardo de Moura
656b642c4a
fix(frontends/lean): identifier size when using unicode
...
see issue #756
2015-07-30 11:32:24 -07:00
Leonardo de Moura
cc4f18c062
feat(frontends/lean): add "--info" command line option for extracting identifier/keyword information
...
see issue #756
2015-07-30 10:18:03 -07:00
Leonardo de Moura
d06c2b1ad3
chore(tests/lua/mod5): remove test that regularly timeout on Windows machines
2015-07-29 18:17:06 -07:00
