Commit graph

4665 commits

Author SHA1 Message Date
Leonardo de Moura
189e5e6b48 refactor(library/data/nat/wf): mark theorem as transparent
It doesn't really help since
        le_imp_lt_or_eq, succ_le_cancel, lt_imp_le_succ and or.elim
are still opaque
2014-11-10 12:52:02 -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
50973bb4f3 feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations
To retrieve the previous behavior, we should use [strict] modifier
2014-11-10 12:46:04 -08:00
Leonardo de Moura
bd5f3ec572 feat(emacs/lean-syntax): highlight [decls] modifier 2014-11-10 10:35:42 -08:00
Leonardo de Moura
363d4a7577 fix(library/definitional/no_confusion): assertion violation 2014-11-10 10:32:03 -08:00
Leonardo de Moura
95554a527c feat(frontends/lean/placeholder_elaborator): display instance trace header once per class-instance resolution problem 2014-11-09 15:00:13 -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
1d9a0a6265 feat(frontends/lean/placeholder_elaborator): add option 'elaborator.instance_max_depth' 2014-11-09 11:59:44 -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
6362610411 fix(frontends/lean): include position information 2014-11-09 11:43:44 -08:00
Leonardo de Moura
76fb6893e1 feat(frontends/lean): add elaborator.trace_instances option
When on this option allows us to visualize "class-instance resolution"
2014-11-09 11:24:19 -08:00
Leonardo de Moura
0b8c44a94a feat(frontends/lean): add option pp.purify_metavars
It is true by default. If the user sets it to false, then
the internal metavariable names are used in the pretty printer
2014-11-09 11:04:22 -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
Soonho Kong
d25e74b921 fix(emacs/lean-mode): remove whitespace-cleanup-mode dependency
- When customization variable 'lean-delete-trailing-whitespace' is
   non-nil, trailing-whitespaces are removed before save.

 - It doesn't change TABs.

Close #226
2014-11-09 00:21:43 -05:00
Soonho Kong
36476b9115 fix(lean-util): handle case where incomplete hierarchical name ends with "."
Close #311
2014-11-08 23:46:59 -05:00
Floris van Doorn
107a9cf8e4 feat(library): port more of truncation library from Coq HoTT
Everything directly about truncations in the basic truncation library is ported.
Some theorems about other structures still need to be ported.
Also made some minor changes in hott.equiv
2014-11-08 19:12:54 -08:00
Floris van Doorn
780e949992 feat(empty): define negation of types 2014-11-08 19:12:54 -08:00
Floris van Doorn
bf27a17dec style(library): add some comments 2014-11-08 19:12:54 -08:00
Floris van Doorn
8c7fdd3708 style(library): rename set_category to discrete_category 2014-11-08 19:12:54 -08:00
Floris van Doorn
930cc11684 doc(algebra): update markdown files 2014-11-08 19:12:54 -08:00
Floris van Doorn
cd33d2e96d refactor(typeof): move typeof to general_notation 2014-11-08 19:12:54 -08:00
Floris van Doorn
74779dd855 feat(hott/trunc): clean up some theorems, prove some basic theorems 2014-11-08 19:12:54 -08:00
Floris van Doorn
08c56188b6 feat(library/hott/trunc): prove that n-types are (n+1)-types. 2014-11-08 19:12:54 -08:00
Jeremy Avigad
4a955c0f92 feat(library/algebra/order): begin theory of orders
feat(library/algebra/order): begin theory of orders
2014-11-08 19:07:59 -08:00
Leonardo de Moura
b97d437011 refactor(library/data/nat/basic): use no_confusion construction to simplify proofs 2014-11-08 19:00:40 -08:00
Leonardo de Moura
ac5a963db3 refactor(library/data/sum): use no_confusion construction to simplify proofs 2014-11-08 18:58:56 -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
46149d0d50 refactor(library/data/prod): break into pieces to reduce dependencies
prod is needed for some automatically generated constructions.
So, it is important it is loaded in the environment as early as possible.
2014-11-08 10:19:29 -08:00
Leonardo de Moura
ad2ecfb7a8 refactor(library/logic/cast): move heq declaration to a separate module
heq is be needed for some automatically generated constructions.
So, we want it available with the least number of dependencies.
2014-11-08 10:19:29 -08:00
Leonardo de Moura
c7992f2cac feat(frontends/lean): add [whnf] modifier to eval command 2014-11-08 10:19:29 -08:00
Soonho Kong
d861c78072 fix(emacs/lean-syntax): change comment symbols to be considered as punctuations
Please read the documentation of "modify-syntax-entry":

"The first character of NEWENTRY should be one of the following:
  _           symbol constituent
  .           punctuation
"

Close: #306
2014-11-07 17:48:21 -05:00
Soonho Kong
18a41eb962 feat(emacs/lean-mode): bind "C-c C-k" to quail-show-key
- Use this to see how to type a unicode character
2014-11-07 17:28:21 -05:00
Leonardo de Moura
64d2cc60c2 feat(library/data/nat/wf): add nat.lt is well founded theorem 2014-11-07 10:48:31 -08:00
Jeremy Avigad
c28227d7a1 feat(library/algebra/group): add multiplicative and additive structures 2014-11-07 10:23:37 -08:00
Jeremy Avigad
05ec76185d fix(library/hott/fibrant): set arguments for type class resolution 2014-11-07 10:23:37 -08:00
Leonardo de Moura
92b0a538c5 refactor(library/logic/wf): add well_founded class, and cleanup file 2014-11-07 10:18:24 -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
fd34fd17de refactor(library/data/bool): break into pieces to reduce dependencies 2014-11-07 08:41: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
8d05238533 fix(kernel/error_msgs): ignore binder information when comparing type mismatches, fixes #304 2014-11-06 21:03:51 -08:00
Leonardo de Moura
ed83b7ff2a fix(emacs/lean-syntax): syntax highlight, issue #306
1- FIXED     structure foo := (bar : Type) -- the name of structures is not highlighted
2- NOT FIXED check foo-- this comment is not highlighted
3- FIXED     check Type.{5} -- Type is not highlighted
4- FIXED     definition bar{thisishighlighted : Type} := foo
5- FIXED     definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo

Have no idea what is going on with 2. I'm not sure if this is our bug,
or Emacs code we depend on.
2014-11-06 20:59:31 -08:00
Jakob von Raumer
754901cf64 fix(library/hott) make universe index in ua.lean variable 2014-11-06 20:02:10 -05:00