Leonardo de Moura
902a551048
feat(definitional/brec_on): add 'mk_below' skeleton
2014-11-11 14:55:21 -08:00
Leonardo de Moura
5fbf9ee964
refactor(library/definitional/util): remove code duplication
2014-11-11 13:53:41 -08:00
Leonardo de Moura
1079d6b320
refactor(library/definitional): combine auxiliary functions used by definitional package in a single module
2014-11-11 13:46:36 -08:00
Leonardo de Moura
b4be96c980
feat(library/definitional/util): add is_inductive_predicate auxiliary predicate
2014-11-11 13:32:56 -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
4fd1ee7619
feat(library/definitional/util): add is_recursive_datatype auxiliary function
2014-11-11 12:26:26 -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
21b93bd2e5
chore(library/data/prod/wf): remove dependency on opaque theorem
2014-11-11 00:39:53 -08:00
Leonardo de Moura
54213b48dc
feat(library/data/prod/wf): lex of well-founded relations is well-founded
2014-11-11 00:29:21 -08:00
Leonardo de Moura
76711d00c1
feat(library/data/nat/wf): define measure using inverse image
2014-11-11 00:28:46 -08:00
Leonardo de Moura
4623a62ec3
feat(library/data/nat/wf): predecessor relation is well-founded
2014-11-10 22:15:15 -08:00
Leonardo de Moura
9c93816211
chore(library/logic/wf): cleanup
2014-11-10 21:19:38 -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
4ebd3e2c27
feat(library/logic/wf): transitive closure of a well-founded relation is well-founded
2014-11-10 21:07:28 -08:00
Leonardo de Moura
22b7a0615f
fix(frontends/lean): coercion affects other modules
2014-11-10 20:14:19 -08:00
Leonardo de Moura
64043094f4
feat(library/logic/wf): some basic definitions for constructing well_founded relations
2014-11-10 17:57:55 -08:00
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
