max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
12235 commits 1 branch 0 tags 5.3 GiB
Commit graph

2797 commits

Author SHA1 Message Date
Leonardo de Moura
499fc355df feat(library/init): add has_well_founded type class 2017-05-17 14:34:52 -07:00
Sebastian Ullrich
84997bf4de refactor(init/meta/expr): unify expr and pexpr 2017-05-17 10:38:12 -07:00
Sebastian Ullrich
5f3e0a1cc4 feat(frontends/lean/decl_cmds): allow implicit locals in constants & axioms 2017-05-17 10:38:12 -07:00
Leonardo de Moura
cb6d5675df chore(library/init): ^. ==> . 2017-05-16 15:00:58 -07:00
Leonardo de Moura
cba0eef101 fix(library/data, library/init/data/array): adjust hash_map PR 2017-05-16 14:46:43 -07:00
Mario Carneiro
422820243d chore(tools/super/utils): remove duplicate partition def 2017-05-16 14:38:43 -07:00
Mario Carneiro
6b28499e47 feat(init/data/list,data/list): new basic list operations from haskell 2017-05-16 14:38:43 -07:00
Mario Carneiro
7257e32eca refactor(init/data/list/lemmas): remove projection notation 2017-05-16 14:38:43 -07:00
Mario Carneiro
69c2c998a7 fix(init/data/list/lemmas): fix references to drop 2017-05-16 14:38:43 -07:00
Mario Carneiro
19a919061f fix(library/data/hash_map): respond to review comments 2017-05-16 14:38:43 -07:00
Mario Carneiro
5d89a93fce feat(library/data/hash_map): verified hash_map 2017-05-16 14:38:43 -07:00
Mario Carneiro
3b89739850 feat(library/data/list, library/data/array): theorems needed for new hash_map 
Note that hash_map is moved to library_dev, where the more advanced theorems on lists are available
 2017-05-16 14:38:43 -07:00
Leonardo de Moura
ed6b7662df feat(library/init/data): add aux lemmas 2017-05-16 14:25:06 -07:00
Leonardo de Moura
8b32f3e7a9 chore(library/init/data/fin/basic): pretty print fin.mk using anonymous constructor notation 2017-05-16 13:54:12 -07:00
Leonardo de Moura
0091cef9f2 feat(library/tactic): start algebraic normalizer 2017-05-15 21:46:19 -07:00
Leonardo de Moura
4575c9e038 feat(frontends/lean): swap (t) and ``(t) semantics 2017-05-15 09:41:31 -07:00
Mario Carneiro
7ace147f25 refactor(init/meta/tactic): replace assertv -> note, definev -> pose 2017-05-14 19:34:27 -07:00
Sebastian Ullrich
27c1d2f4fb fix(init/meta/interactive): simp: accept local refs as simp names 2017-05-14 19:19:22 -07:00
Sebastian Ullrich
eb60df4409 fix(init/meta/interactive): case didn't find some cases 2017-05-14 19:19:22 -07:00
Sebastian Ullrich
808ab73d93 refactor(init): use list for expr.macro args 2017-05-14 19:17:28 -07:00
Sebastian Ullrich
42eb0c680e feat(kernel/inductive,library/inductive_compiler): do not enforce positivity rule on meta inductives 2017-05-14 19:17:28 -07:00
Sebastian Ullrich
171a96a8de refactor(library): remove all instances of `(...) 2017-05-12 19:13:48 +02:00
Sebastian Ullrich
4b21b13649 refactor(init): replace has_quote class with reflected 2017-05-09 16:02:42 -07:00
Sebastian Ullrich
ead6318ee0 feat(frontends/lean/elaborator): substitute reflected locals into expr quotes 2017-05-09 16:02:41 -07:00
Sebastian Ullrich
2825c5fbcc feat(frontends/lean/elaborator): elaborate ``(e) to type reflected e` if possible and add coercion reflected -> expr 2017-05-09 16:02:41 -07:00
Joe Hendrix
216d619d90 chore(library/init/data/nat): Remove [simp] from nat.pow_succ 2017-05-08 10:15:43 -07:00
Gabriel Ebner
4b22e2309c refactor(system/io): use spawn_args structure in all process functions 2017-05-04 16:41:11 -07:00
Gabriel Ebner
f0d22ed3e5 feat(library/process,system/io): set environment variables for spawned processes 2017-05-04 16:41:11 -07:00
Gabriel Ebner
c4aef89296 feat(system/io): add finally combinator 2017-05-04 16:41:11 -07:00
Gabriel Ebner
1b8533130b feat(system/io): add function to get environment variables 2017-05-04 16:41:11 -07:00
Daniel Selsam
d727abeefc chore(library/inductive_compiler/nested.cpp): prove all theorems in C++ 2017-05-04 16:34:32 -07:00
Sebastian Ullrich
d0c2c73b35 refactor(init/meta,tools): rename now tactic to done 
It was pointed out that Coq already uses `now` for a different kind of tactic.
And `done` is more descriptive anyway.
 2017-05-03 11:18:31 +02:00
Leonardo de Moura
73b4e42485 chore(frontends/lean,library): fix character pretty printer 2017-05-02 13:17:22 -07:00
Leonardo de Moura
a0a8103804 chore(frontends/lean): go back to 'c' as notation for characters 
This suggestion has been discussed at Slack.
We have decided to use #"c" as notation because we wanted to allow `'`
in the beginning of identifiers like in SML and F*. In particular,
we wanted to allow users to use 'a 'b 'c for naming type parameters
like in SML. However, nobody used this notation. In the Lean standard
library, we are using greek letters for naming type parameters.
So, there is no real motivation for the ugly #"c" syntax.
 2017-05-02 13:00:51 -07:00
Leonardo de Moura
55fee26b36 feat(library/class): add attribute for tracking symbols occurring in instances of type classes 
For more information see:
https://github.com/leanprover/lean/wiki/Refactoring-structures
The new attribute [algebra] implements the [algebraic_class] described
in the page above.
 2017-05-01 18:02:30 -07:00
Gabriel Ebner
ed9e7d9066 feat(leanpkg): make add command more awesome 2017-05-01 14:11:39 -07:00
Gabriel Ebner
c744efe2f5 feat(leanpkg): add package manager 2017-05-01 14:11:38 -07:00
Gabriel Ebner
fd6407eccb feat(library/data/buffer/parser): parser combinators for char_buffer 2017-05-01 14:11:38 -07:00
Gabriel Ebner
c46ffbde4c feat(library/init/data/char): character class predicates 2017-05-01 14:11:38 -07:00
Gabriel Ebner
867c38e1ea feat(library/data/buffer,library/init/data/array): utility functions on buffers 2017-05-01 14:11:38 -07:00
Leonardo de Moura
ba5eccdca8 refactor(library/init/core): rename out_param => inout_param 
It is really input/output.
 2017-05-01 14:01:41 -07:00
Leonardo de Moura
74550fbebc feat(library/init/core): add notation for out_param 2017-05-01 13:52:17 -07:00
Leonardo de Moura
949ed3ac5c feat(library/init/category/applicative): add has_seq type classes 2017-05-01 12:57:05 -07:00
Leonardo de Moura
f6b47ea5c7 feat(library/init/category): add has_map type class, delete fmap 2017-05-01 10:13:02 -07:00
Leonardo de Moura
66a1fec94e feat(library/init/category): add has_orelse type class 2017-05-01 09:58:27 -07:00
Leonardo de Moura
5cef84709f refactor(library): avoid auxiliary definitions such as add/mul/le/etc 
See Section "Other goodies" at
https://github.com/leanprover/lean/wiki/Refactoring-structures

This commit also improves the support for projections in the
unifier/matcher.

Now, we consider the extra case-split for projections.
Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce.
This is needed in the standard library because we now have constraints such as:
```
@has_le.le ?A ?s ?a ?b  =?=  @has_le.le nat nat.has_add x y
```
If we reduce the right hand side, we get the unsolvable constraint
```
@has_le.le ?A ?s ?a ?b  =?=  nat.le x y
```
Before this change, the constraint was `@le ?A ?s ?a ?b  =?=  @le nat nat.has_add x y`, and we already perform a case-split in this case.
Moreover, projections were eagerly reduced whenever possible.
The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out.
I worked around this issue by performing the case-split only when the constraint contains meta-variables.
There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`.
 2017-05-01 08:52:19 -07:00
Leonardo de Moura
701b51a882 chore(library/tools/mini_crush/default): increase timeout 2017-04-30 16:27:55 -07:00
Leonardo de Moura
fc9a8ed3be fix(library/init/meta/smt): fail tactic result type 2017-04-30 14:39:51 -07:00
Sebastian Ullrich
0ca6e2c96f refactor(library/{type_context,compiler/preprocess},frontends/lean/elaborator): use opaque, general type class instead of special app elaboration for eval_expr 2017-04-27 16:04:59 -07:00
Sebastian Ullrich
4479eebaf0 feat(init/meta/{environment,pexpr}): expose some structure APIs 2017-04-27 16:04:41 -07:00