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
Jakob von Raumer
b8ec1a1649
chore(library/hott) cleanup
2014-11-06 19:41:08 -05:00
Jakob von Raumer
f1cc0c4bd8
chore(library/hott) add note referring to missing substitution lemma
2014-11-06 19:27:27 -05:00
Jakob von Raumer
7dbd7b31f6
Added substitution lemma for equivalence calculations
2014-11-06 19:22:57 -05:00
Jakob von Raumer
fa9cbb1f6a
chore(library/hott) adapted univalence axiom to suit notation in book and def in Coq.
2014-11-06 19:22:57 -05:00
Jakob von Raumer
d842be9c52
feat(library/hott) add univalence axiom
2014-11-06 19:22:57 -05:00
Jakob von Raumer
28d1c6c5e4
chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it
2014-11-06 19:22:57 -05:00
Jakob von Raumer
9ad75108a3
chore(library/hott) clean up file and add class inference
2014-11-06 15:57:30 -08:00
Jakob von Raumer
1f5be44f51
chore(library/hott) clean up Equiv namespace
2014-11-06 15:57:30 -08:00
Jakob von Raumer
8e1949e9aa
feat(library/hott) add calc environment for equivalences
2014-11-06 15:57:29 -08:00
Jakob von Raumer
c50db9899d
feat(library/hott) add thm: to give a section of a fibration it suffices to provide it for the image of an equivalence
2014-11-06 15:57:29 -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
