michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
7113 commits 3 branches 0 tags 28 MiB
Commit graph

4996 commits

Author SHA1 Message Date
Leonardo de Moura
98bfb8467a test(test/shared): add small program for testing shared library 2015-08-13 11:48:54 -07:00
Leonardo de Moura
8746484b8f fix(CMakeLists): DLL generation 2015-08-13 11:38:33 -07:00
Leonardo de Moura
498afc1e6f feat(CMakeLists): add shared library 2015-08-13 11:21:05 -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
Soonho Kong
6443de67d4 feat(emacs/lean-mode): lean-exec-at-pos uses timer to wait until flycheck process is over 
close #790
 2015-08-11 20:17:53 -04:00
Daniel Selsam
40471ca8e3 doc(frontends/lean/elaborator): assert invariant in visit_app 2015-08-11 17:02:38 -07:00
Leonardo de Moura
23118371d1 refactor(library/aliases): cleanup 2015-08-11 06:41:56 -07:00
Soonho Kong
00582934ec feat(CMakeLists.txt): update CXX_FLAGS_EMSCRIPTEN 
Add: -O3 -s ALLOW_MEMORY_GROWTH=1 --llvm-lto 1

Close leanprover/tutorial#96
 2015-08-10 02:03:39 -04:00
Soonho Kong
938dae7b19 refactor(emacs/lean-syntax.el): clean up regexps for syntax 2015-08-08 09:55:16 -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
Jeremy Avigad
d6bde18b46 feat,refactor(library/data/{finset,set}/*,src/emacs/lean-input.el): add powerset and notation, and some tidying 2015-08-07 13:45:15 -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
Soonho Kong
f9b069b6a5 fix(emacs/lean-company.el): set timeout for company-lean--import-candidates 
Custom variable lean-company-import-timeout is added (default: 1sec).

Close #766
 2015-08-06 22:53:49 -04:00
Soonho Kong
a4014fb532 feat(emacs/lean-util.el): add lean-find-files 2015-08-06 22:48:00 -04:00
Soonho Kong
7d1895928a fix(emacs/lean-mode.el): use original extension when make temp-file 
close #767
 2015-08-05 12:51:09 -04:00
Soonho Kong
795728267d doc(emacs/README.md): update MELPA instruction 2015-08-03 09:27:16 -04:00
Leonardo de Moura
60ba3d15ff feat(library/data/matrix): add basic matrix module 2015-08-01 19:33:31 +01: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
8f5a760b89 feat(frontends/lean/elaborator): display the whole proof state in option "--goal" 
see issue #755
 2015-07-31 08:56:17 -07:00
Leonardo de Moura
f264adfa92 fix(library/export): bug in --export-all option 2015-07-30 17:23:38 -07:00
Leonardo de Moura
9bf64c10fd feat(library/export): export the whole environment when using "--expor-all" 2015-07-30 15:04:49 -07:00
Soonho Kong
bed751a2d7 feat(emacs/lean-settings.el): add lean-keybinding customize group 
close #758
 2015-07-30 11:33:17 -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
a39cac4fad feat(frontends/lean): improve '--info' command line option 
see issue #756
 2015-07-30 11:05:39 -07:00
Soonho Kong
c390550340 feat(emacs/lean-mode.el): add show-goal-at-pos and show-id-keyword-info in the menu 2015-07-30 10:46:47 -07:00
Soonho Kong
46a79ec43d feat(emacs/lean-mode.el): add lean-show-id-keyword-info 
close #756
 2015-07-30 10:46:10 -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
be61fb0566 feat(frontends/lean/elaborator): add "noncomputable theory" command, display "noncomputable" when printing definitions 
When the command "noncomputable theory" is used, Lean will not sign an
error when a noncomputable definition is not marked as noncomputable
 2015-07-29 17:54:35 -07:00
Leonardo de Moura
384ccf2b6c feat(frontends/lean/elaborator): change behavior of "show goal" for incomplete "by tactic" 
If "by tactic" did not completely solved the goal, then we show the
final state when the user presses "C-c C-g"
 2015-07-29 17:34:42 -07:00
Leonardo de Moura
b3707ab54a feat(library/tactic/unfold_rec): fixes #753 2015-07-29 17:13:02 -07:00
Leonardo de Moura
ed41a01a51 fix(frontends/lean/elaborator): fixes #755 2015-07-29 16:41:30 -07:00
Leonardo de Moura
0bda39c8ac feat(frontends/lean): check for noncomputability when moving theorems from theorem_queue to environment 2015-07-29 13:01:07 -07:00
Leonardo de Moura
69ead0ddd8 feat(frontends/lean/decl_cmds): reject unnecessary "noncomputable" annotations 2015-07-29 13:01:07 -07:00
Leonardo de Moura
74be3031b1 feat(frontends/lean/decl_cmds): sign an error if "noncomputable" keyword is used in the HoTT library or with non-definitions 2015-07-29 13:01:06 -07:00
Soonho Kong
8a9f774611 fix(emacs/lean-mode.el): lean-exec-at-pos don't ask to save 
close #752
 2015-07-29 10:28:18 -07:00
Soonho Kong
5d159ea664 fix(emacs/lean-mode.el): fix wrong parens in lean-show-goal-at-pos 2015-07-28 22:11:35 -07:00
Leonardo de Moura
308af87b69 feat(library): add 'noncomputable' keyword for the standard library 2015-07-28 21:56:35 -07:00
Leonardo de Moura
a009db2902 feat(library): add module for tracking noncomputable definitions 2015-07-28 18:15:26 -07:00
Leonardo de Moura
7e8a394caf chore(tests/lean): fix style and adjust tests 2015-07-28 18:15:25 -07:00
Leonardo de Moura
b81d4d50f1 feat(frontends/lean/bultin_cmds): add 'print axioms <declname>' command that prints axioms a giving declaration depends on 2015-07-28 18:15:25 -07:00
Leonardo de Moura
8048cbd6f2 feat(kernel): do not hide semi-constructive axioms 2015-07-28 18:15:25 -07:00
Soonho Kong
1829e64a76 feat(emacs/lean-server.el): lean-server-consume-all-async-tasks restart lean-server if necessary 
related issue: #263
 2015-07-28 18:14:16 -07:00
Leonardo de Moura
80e3da0526 fix(library/util): fixes #751 2015-07-28 16:30:20 -07:00
Leonardo de Moura
ad5d792a8e feat(library,shell): add --export-all command line option 2015-07-28 15:54:44 -07:00
Soonho Kong
a5da840593 fix(emacs/lean-mode.el): typo 2015-07-28 14:46:59 -07:00
Soonho Kong
0fed6129df feat(emacs/lean-mode): add lean-show-goal-at-pos 
which is bound to 'C-c C-g' by default. Depending on the current char,
it invokes lean-server with either '--goal' or '--hole' option.

close #749
 2015-07-28 14:17:36 -07:00
Leonardo de Moura
cfa9412f96 fix(frontends/lean): "show goal" localization, add "position", support "by tactic" 2015-07-28 12:48:12 -07:00
Leonardo de Moura
0dc8dc999e fix(library/tactic/rewrite_tactic): crash when trying to unfold constructor 2015-07-28 12:43:56 -07:00
Soonho Kong
f71987612f fix(emacs/lean-syntax.el): update lean-info syntax highlight 
close #748
 2015-07-28 11:51:01 -07:00
Soonho Kong
72f0fc29fd fix(emacs/lean-mode.el): check header and footer in lean-exec-at-pos-extract-body 
close #747
 2015-07-28 11:13:31 -07:00
Leonardo de Moura
08b23d8b4f test(tests/lean/extra): add test for "show goal" feature 2015-07-27 21:03:16 -07:00
Soonho Kong
e61a61da8b feat(emacs/lean-mode.el): use lean-info-mode in lean-exec-at-pos 2015-07-27 20:26:28 -07:00
Leonardo de Moura
91f83835bb fix(frontends/lean/elaborator): "show goal" command line option for nested "begin...end" blocks 2015-07-27 20:11:27 -07:00
Soonho Kong
a9630edfed feat(emacs/lean-mode.el): handle delimiter for lean-exec-at-pos 
Related issue: #499
 2015-07-27 19:28:16 -07:00
Daniel Selsam
ee11fca69b refactor(src/library/export): disambiguate export keywords 2015-07-27 19:08:26 -07:00
Leonardo de Moura
b4504357b2 fix(shell/lean): do not update cache file in query mode 
query mode is "show goal" and "show hole" command line options
 2015-07-27 19:00:36 -07:00
Leonardo de Moura
d50fa26ca2 fix(frontends/lean/parser): caching problem when using "show hole" and "show goal" command line options 2015-07-27 18:55:20 -07:00
Leonardo de Moura
0786841c71 feat(frontends/lean): use uniform delimiter 2015-07-27 18:45:33 -07:00
Leonardo de Moura
3fb16d6287 feat(frontends/lean): add "show hole" command line option 2015-07-27 18:42:57 -07:00
Leonardo de Moura
68370d5c8e feat(frontends/lean): process "show goal" command line option 2015-07-27 17:44:43 -07:00
Daniel Selsam
214b5b8b58 refactor(src/library/export): prefix export keywords with # 2015-07-27 15:07:12 -07:00
Leonardo de Moura
b2bd6b1ff8 feat(library/simplifier): simplification sets for hypothesis and conclusion 2015-07-27 14:59:21 -07:00
Leonardo de Moura
966e0109ff feat(library/simplifier): initialize simplification set. 2015-07-27 14:59:21 -07:00
Leonardo de Moura
4131bb3dec feat(util/name_set): add to_name_set auxiliary function 2015-07-27 14:59:21 -07:00
Soonho Kong
6de86ff749 fix(emacs/lean-mode.el): attach sentinel to lean-exec-at-pos 
Close #499

Usage:

(add-hook 'lean-mode-hook '(lambda ()
(lean-define-key-binding "\C-c\C-g"
                     '(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))))
 2015-07-27 13:17:16 -07:00
Leonardo de Moura
5c7a20e5bd fix(library/unifier): crash when unifying constraints of the form (pr t =?= s) 
where pr is a projection and t is a stuck term

see issue #737
 2015-07-24 11:52:46 -07:00
Leonardo de Moura
bcf057f4f3 feat(frontends/lean): display '[congr]' attribute when printing theorems 2015-07-23 18:52:59 -07:00
Leonardo de Moura
3e6b80d38c feat(library/util): disable local constant purification when pretty printing goals 
This feature generates confusion.
 2015-07-23 18:52:59 -07:00
Leonardo de Moura
f1a19a10c4 fix(library/util): incorrect hypothesis renaming when pretty printing goals 2015-07-23 18:52:59 -07:00
Leonardo de Moura
e221d38790 feat(library/tactic/assert_tactic): allow duplicate names for hypotheses in assert tactic 2015-07-23 18:52:59 -07:00
Leonardo de Moura
e0209a1532 feat(frontends/lean): better error localization for 'have'-expressions in tactic mode 2015-07-23 18:52:59 -07:00
Leonardo de Moura
946308b187 feat(frontends/lean): allow anonymous 'have'-expressions in tactic mode 2015-07-23 18:52:59 -07:00
Leonardo de Moura
5f4576a7f7 test(tests/lean): add test for '[congr]' attribute validation 2015-07-23 18:52:59 -07:00
Leonardo de Moura
844caf32e4 feat(frontends/lean/bultin_cmds): add 'print [congr]' command for displaying active congruence rules 2015-07-23 18:52:59 -07:00
Leonardo de Moura
3329dc0ec7 feat(library/simplifier/simp_rule_set): add '[congr]' attribute validation 2015-07-23 18:52:58 -07:00
Leonardo de Moura
933f056fff feat(library/simplifier): add API for extracting simplification rules defined in a given namespace 2015-07-22 18:47:56 -07:00
Leonardo de Moura
18dd7c13f9 feat(frontends/lean): add '[congr]' attribute 2015-07-22 17:21:47 -07:00
Leonardo de Moura
a07b42ad9e refactor(library/simplifier): the simplifier expects relations to be transitivie and reflexive 2015-07-22 15:46:00 -07:00
Leonardo de Moura
cc396cba76 feat(frontends/lean): allow backticks in binder declarations 2015-07-22 13:54:47 -07:00
Leonardo de Moura
8085123119 refactor(library/simplifier): rename 'rewrite_rule' to 'simp_rule' 2015-07-22 10:39:30 -07:00
Leonardo de Moura
e969c7a8d6 refactor(library): remove 'simp' hack 2015-07-22 10:13:19 -07:00
Leonardo de Moura
092c8d05b9 feat(frontends/lean,library): rename '[rewrite]' to '[simp]' 2015-07-22 09:01:42 -07:00
Leonardo de Moura
b5c287d3d1 refactor(library/simplifier): cleanup 2015-07-22 08:39:55 -07:00
Leonardo de Moura
e74c6eef3d feat(library/simplifier): add 'simp.funext' and 'simp.propext' options 2015-07-21 18:23:10 -07:00
Leonardo de Moura
0c0f07332e feat(library/simplifier/simp_tactic): add simp tactic configuration options 2015-07-21 16:15:04 -07:00
Leonardo de Moura
b02b3d362f feat(library/simplifier): add simplifier procedure skeleton 2015-07-21 15:08:56 -07:00
Leonardo de Moura
9a85a95893 fix(cmake/Modules/CleanOlean.cmake): problem with 'clean-olean' 
For some reason it was not working anymore on OSX
 2015-07-20 23:21:51 -07:00
Leonardo de Moura
b9451549d1 feat(frontends/lean): add type notation for referencing hypotheses 2015-07-20 21:43:47 -07:00
Leonardo de Moura
18dd57978d feat(CMakeLists.txt): .dmg generation 2015-07-20 20:33:33 -07:00
Leonardo de Moura
a99c44b644 fix(CMakeLists.txt): disable problematic tests on Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-07-20 08:14:31 -07:00
Leonardo de Moura
812ddf1ef5 feat(frontends/lean): add 'suppose'-expression 
It is a variant of 'assume' that allow anonymous declarations.
 2015-07-19 12:15:12 -07:00
Leonardo de Moura
92f8eb173b feat(frontends/lean): use 'this' as the name for anonymous 'have'-expression 2015-07-18 13:36:05 -05:00
Soonho Kong
c72e661a9e feat(CMakeLists.txt): add option USE_GITHASH (default:on) 
related issue: #733
 2015-07-17 16:55:22 -04:00
Soonho Kong
014a5ea83e fix(emacs/load-lean.el): add let-alist 
close #729
 2015-07-15 16:07:35 -07:00
Leonardo de Moura
f5c546e810 feat(frontends/lean/parse_simp_tactic): add simp tactic parser 2015-07-14 14:21:39 -04:00
Leonardo de Moura
3ab0e07ba9 feat(frontends/lean): add simp tactic frontend stub 
This commit also removes the fake_simplifier. It doesn't work anymore
because simp is now a reserved word.
 2015-07-14 09:54:53 -04:00
Leonardo de Moura
84b439507b chore(library/tactic): fix style 2015-07-13 19:43:33 -04:00
Leonardo de Moura
c2edc330ef fix(library/tactic/rewrite_tactic): remove incorrect assertion 2015-07-13 19:19:12 -04:00
Leonardo de Moura
267545ca0c feat(frontends/lean): parse 'with_options' tactical 
see issue #492
 2015-07-13 19:13:41 -04:00
Leonardo de Moura
9c5bf98ed6 feat(library/tactic): add 'with_options' tactical 
see issue #494
 2015-07-13 18:34:31 -04:00
Leonardo de Moura
0f714e36b0 feat(library/tactic): add 'location' macro 2015-07-13 17:56:42 -04:00
Leonardo de Moura
58291024a9 fix(library/simplifier/ceqv): polish conditional rewrite internalization procedure 2015-07-13 16:40:18 -04:00
Leonardo de Moura
3cb8568fb5 feat(library/simplifier): we can "rewrite" with transitive relations 
The simplifier does not really need the relation to be an equivalence.
Transitivity is the main required property (we need to chain rewrites
together).
 2015-07-12 14:24:05 -04:00
Leonardo de Moura
f8d472c9f1 feat(frontends/lean/parse_rewrite_tactic): change the semantics of rewrite[↑f] when f is recursive 
After this commit it behaves like 'unfold f'.
That is, it will unfold f even if it fails to fold recursive
applications. Now, only 'esimp[f]' will not unfold f-applications when
it cannot fold the recursive applications.

This commit also closes #692. It is part of a series of commits that
addresses this issue.

closes #692
 2015-07-12 13:20:21 -04:00
Leonardo de Moura
4c0a656ecc fix(library/tactic/unfold_rec): support indexed families + brec_on at unfold_rec 
see issue #692
 2015-07-12 12:45:05 -04:00
Leonardo de Moura
584f9e3f49 fix(library/tactic/unfold_rec): support indexed families at unfold_rec 
This commit also removes many (now unnecessary) folds from the HoTT
library.

See issue #692

We still have to implement support for recursive definitions based on
brec_on that recurse over inductive families.
 2015-07-12 12:32:58 -04:00
Leonardo de Moura
7fa5c3e5da feat(library/tactic/unfold_rec): take '[recursor]' annotations into account at unfold_rec 2015-07-12 11:33:40 -04:00
Leonardo de Moura
b0ac78c2cb feat(library/user_recursors): add is_user_defined_recursor predicate 2015-07-12 11:25:50 -04:00
Leonardo de Moura
8e8e08cfe7 feat(library/tactic): use occurrence object in unfold tactic family 2015-07-11 18:53:45 -04:00
Leonardo de Moura
554a42b407 fix(library/tactic/unfold_rec): add annother brec pattern that should be checked in the unfold recursive definition tactic 2015-07-10 22:16:23 -04:00
Leonardo de Moura
a9515ac7a4 feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function 
See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.
 2015-07-08 21:19:18 -04:00
Leonardo de Moura
967f9ece8e fix(frontends/lean/notation_cmd): workaround incorrect warning produced by clang++ on OSX 2015-07-07 21:01:48 -07:00
Leonardo de Moura
6ffbb05118 feat(library/definitional/no_confusion): add [unfold] hint to no_confusion 2015-07-07 20:07:13 -07:00
Leonardo de Moura
26574e29a9 feat(library/normalize,frontends/lean): allow multiple arguments in [unfold] hint 
closes #693
 2015-07-07 18:01:57 -07:00
Leonardo de Moura
a27b20cd9c feat(frontends/lean/notation_cmd): allow local notation to override reserved notation 
closes #712
 2015-07-07 17:30:46 -07:00
Leonardo de Moura
4b1b3e277f feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]' 
see issue #693
 2015-07-07 16:37:06 -07:00
Leonardo de Moura
991ff67b45 refactor(library/relation_manager): cleanup and add API for declaring a relation that may not be reflexive, symmetric nor transitive 2015-07-07 15:58:24 -07:00
Leonardo de Moura
fb833a724b fix(src/frontends/lean/parser): add extra annotations to workaround with clang 6.0.0 2015-07-06 16:39:47 -07:00
Leonardo de Moura
b0c56273e2 fix(frontends/lean/elaborator): fixes #724 2015-07-06 15:19:19 -07:00
Leonardo de Moura
c843690d27 fix(frontends/lean/elaborator): fixes #719 2015-07-03 12:37:28 -07:00
Leonardo de Moura
7de7c5b73d feat(library/definitional/projection): define projections using auxiliary macro 2015-07-02 10:49:49 -07:00
Leonardo de Moura
c15bcf1354 refactor(library/projection): remove projection macro from library 2015-07-02 08:48:13 -07:00
Leonardo de Moura
dd145926a2 fix(library/coercion): compilation warning 2015-07-02 07:26:00 -07:00
Leonardo de Moura
4ae9f3ea81 feat(library/coercion): new coercion manager 
closes #668
 2015-07-01 16:32:34 -07:00
Leonardo de Moura
fe26c37fcb refactor(library/tc_multigraph): improve tc_multigraph API 2015-07-01 16:01:40 -07:00
Leonardo de Moura
765865ed41 chore(library/tc_multigraph): remove dead code 2015-07-01 15:48:55 -07:00
Leonardo de Moura
d44d576194 refactor(library/coercion): simplify coercion module API 2015-07-01 14:40:12 -07:00
Leonardo de Moura
d5c38777af refactor(library/coercion): simplify coercion_class 2015-07-01 14:29:23 -07:00
Leonardo de Moura
0f5b7a36f5 chore(library/coercion): remove lua bindings for coercion module 
Reason: we will refactor the coercion module.
See issue #668
 2015-07-01 14:08:49 -07:00
Leonardo de Moura
667f647b27 feat(kernel/expr_eq_fn): add small optimization 2015-07-01 09:19:36 -07:00
Leonardo de Moura
cabe30ba71 feat(frontends/lean): allow user to assign priorities to notation declarations 2015-06-30 17:10:27 -07:00
Leonardo de Moura
a1d1a8272a refactor(frontends/lean): move parse_priority to util 2015-06-30 16:22:52 -07:00
Leonardo de Moura
4ea57196ff chore(frontends/lean/parser_config): remove dead code 2015-06-30 16:04:00 -07:00
Leonardo de Moura
880f212494 feat(library/class): allow transitive instances that have instances arguments 2015-06-30 14:54:12 -07:00
Leonardo de Moura
9a9e975bc8 feat(frontends/lean/migrate_cmd): ignore derived transitive instances in the migrate command 2015-06-30 14:00:41 -07:00
Leonardo de Moura
d20f831602 feat(library/class): add is_derived_trans_instance predicate 2015-06-30 13:59:02 -07:00
Leonardo de Moura
e7c3c887b6 feat(kernel/type_checker): add 'check' procedure that uses 'opaque_hints' 
The hints only affect performance. If a declaration type checks assuming
some constants are opaque, it should also type check without this
assumption. Of course, it may be much slower.
 2015-06-30 13:12:34 -07:00
Leonardo de Moura
772ed111e5 refactor(kernel): move extra_opaque_converter to kernel, and rename it to hint_converter 2015-06-30 12:59:28 -07:00
Leonardo de Moura
e635d9be9f refactor(kernel): rename get_weight to get_height at declaration 
Motivation:
- It is the standard name for the concept: declaration height
- Avoid confusion with the expression weight
 2015-06-30 12:59:10 -07:00
Leonardo de Moura
1e6550eda6 feat(kernel/default_converter): take into account the 'theorem' annotations in the converability checker 
The idea is that we should seldon need to unfold theorems.
The convertability checker should use that.
When the convertability checker was implemented, theorems were opaque in
Lean. So, this hint was not needed.

This modification is another workaround for the performance problem with
the migrate command at library/data/real/division.lean.
This solution is better than applying proof irrelevance eagerly because
it also addresses similar problems in the HoTT library which does not
support proof irrelevance.

This commit also enables the conv_opt for all theorems.
 2015-06-30 10:42:26 -07:00
Leonardo de Moura
acc0832928 feat(kernel/default_converter): add "eager" proof irrelevance optimization 2015-06-29 19:10:39 -07:00