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
Leonardo de Moura
f4ebd38ce3
feat(frontends/lean/builtin_exprs): improve infix paren notation
...
After this commit, `(+)` is notation for (add) instead of `(fun x y, add x y)`.
This change is relevant when defining type class instances such as
```lean
instance semigroup_to_is_associative [semigroup α] : is_associative α (*) :=
⟨mul_assoc⟩
```
2017-04-27 12:33:33 -07:00
Leonardo de Moura
cabb4350d9
feat(library): instances are not reducible by default anymore
...
Motivation: see "Other goodies" section at
https://github.com/leanprover/lean/wiki/Refactoring-structures
We had to add a new transparency mode: Instances at type_context.
In this mode, instances and reducible definitions are considered
transparent.
The new mode is used in the defeq_canonizer, code generator,
and sizeof lemma generation at inductive_compiler.
We also use the new mode in the unfold tactics.
2017-04-26 14:10:11 -07:00
Leonardo de Moura
08e094139d
feat(library/init/meta): add by_contradiction and by_cases to tactic.interactive
2017-04-26 12:54:52 -07:00
Johannes Hölzl
b27100ec5a
fix(library/init/meta/transfer): add check if target contains (universe) meta variables (see #1535 )
2017-04-25 17:46:48 -07:00
Leonardo de Moura
cdafd4b791
chore(library): cleanup proofs
2017-04-25 17:23:42 -07:00
Sebastian Ullrich
e9a6c544af
refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields
2017-04-24 19:35:15 +02:00
Mario Carneiro
7ef4428124
add new interactive tactics skip, ginduction, exacts
2017-04-23 11:48:33 -07:00
Mario Carneiro
5e8572b407
add set.Union and set.univ
2017-04-23 11:37:27 -07:00
Jared Roesch
4704b68035
chore(*): remove smt2 bindings from standard libary
2017-04-23 11:32:11 -07:00
Joe Hendrix
17291b8a33
refactor(library/data/vector): allow tail to accept empty vector.
2017-04-23 11:22:09 -07:00
Leonardo de Moura
e7603df514
feat(library/init/algebra): add type classes for algebraic normalizer
2017-04-18 15:47:38 -07:00
Sebastian Ullrich
b3884d5f42
refactor(init/meta/interactive,frontends/lean/token_table): introduce generalizing keyword in Lean
2017-04-16 15:11:49 -07:00
Leonardo de Moura
f6556ecdcc
fix(library/init): missing has_sizeof instances for subtype, char and string
2017-04-15 23:31:14 -07:00
Leonardo de Moura
210b7c8fb7
fix(library/tactic): fixes #1513
...
Implement rename tactic in Lean using revert/intro
2017-04-15 11:34:24 -07:00
Leonardo de Moura
e40dbffba9
chore(library): add auxiliary lemmas for hoare state monad experiment
2017-04-12 18:01:59 -07:00
Sebastian Ullrich
8ea2bc08cb
feat(init/meta/interactive): add generalizing parameter to induction
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
4483e53de0
feat(init/util): tactic.trace-like trace_val function
...
Calling it `trace` and removing the old `trace` function does bad things with overloading
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
70a2c402ac
feat(init/meta/interactive): Isabelle-like case tactic
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
c8c8c27654
feat(init/meta): add has_to_format instances and prefer direct has_to_tactic_format implementations
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
026c5ee509
fix(library/init/meta/expr,library/vm/vm_expr): fix macro args
2017-04-11 17:07:28 -07:00
Gabriel Ebner
66cd4c57cf
feat(library/system/io): alternative instance for io
2017-04-11 16:42:17 -07:00
Gabriel Ebner
cefc26d9cb
refactor(library/system/process): add exit status and working directory
2017-04-11 16:42:17 -07:00
Gabriel Ebner
e2fa363423
feat(library/system/io,shell/lean): add --run switch
2017-04-11 16:41:30 -07:00
Leonardo de Moura
6c68aeee01
feat(library/system/io): add io.iterate primitive
2017-03-31 11:34:09 -07:00
Leonardo de Moura
ad859817b1
feat(frontends/lean): allow local decls to shadow namespaces
2017-03-29 16:09:45 -07:00
Leonardo de Moura
35eba0107e
chore(library/init/algebra/ring): use . notation
2017-03-28 18:49:35 -07:00
Johannes Hölzl
c4c2d703f6
feat(library/init/data): simplify int.transfer; add int and nat to zero_ne_one_class
2017-03-28 18:44:56 -07:00
Johannes Hölzl
2c85bb5a4d
feat(library/init/logic): generalize implies_true_iff
...
this generalizes the domain of implies_true_iff from `Prop` to all `Sort`.
With this there is no need for `intros; trivial` after `simp`.
2017-03-28 18:44:56 -07:00
Johannes Hölzl
bc0dbf0809
feat(library/init/algebra): add zero_ne_one and one_ne_zero to default simp-set
2017-03-28 18:44:56 -07:00
Leonardo de Moura
0fe3e3e88f
chore(library): use . notation
2017-03-28 18:42:32 -07:00
Jared Roesch
dc4086d0ed
feat(library/vm/process): add basic process support
2017-03-28 18:08:06 -07:00
Leonardo de Moura
cb049f42b7
fix(frontends/lean/elaborator): resolve_local_name
2017-03-28 17:57:13 -07:00
Leonardo de Moura
71685e4dd6
feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term
...
Replace `^.` with `.` in the stdlib
2017-03-28 17:47:49 -07:00
Leonardo de Moura
87932f1c56
feat(frontends/lean): change notation for inaccessible patterns
...
The following are accepted
.(t)
._
We don't accept .t anymore because it will conflict with the field
access notation.
2017-03-28 16:09:15 -07:00
Leonardo de Moura
6183c7676e
feat(frontends/lean): use . for field access
2017-03-28 15:29:54 -07:00
Leonardo de Moura
8e2dcb8ad8
chore(frontends/lean): remove ^. variants (~> and ↣)
...
This modification was motivated by a discussion at slack.
2017-03-28 12:23:33 -07:00
