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 |
|
Leonardo de Moura
|
1cef8af1be
|
feat(library/tactic/simplify): add eta := tt to simp
|
2017-03-27 17:38:40 -07:00 |
|
Leonardo de Moura
|
eea46610ea
|
fix(library/tactic/simplify): missing projection reduction, add proj := tt to simp
|
2017-03-27 17:38:40 -07:00 |
|
Leonardo de Moura
|
161879b1bf
|
feat(library/init/meta): add helper tactic guard_target for generating tests
|
2017-03-27 17:38:40 -07:00 |
|
Leonardo de Moura
|
b09968a37b
|
feat(library/tactic/simplify): add beta := tt to simp
|
2017-03-27 17:38:31 -07:00 |
|
Leonardo de Moura
|
494e5b65c5
|
feat(library/init/meta/tactic): add apply_auto_param and apply_opt_param tactics
see #1485
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
9e8ef54402
|
refactor(init/data/list/instances): simplify proofs
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
b3a0eb9bfc
|
fix(init/meta/interactive): mk_simp_set: also remove equational lemmas
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
c7b47c7b7f
|
fix(system/io): try to fix io monad
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
dfd84666e2
|
feat(library): add functor, applicative, and monad laws, and prove them correct for non-meta instances
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
b51e666bda
|
feat(init/category/monad): simplify monad.seq._default
|
2017-03-27 13:42:08 -07:00 |
|
Sebastian Ullrich
|
3ead6be9ca
|
feat(init): add default value proofs to the monadic hierarchy
|
2017-03-27 13:42:08 -07:00 |
|
Leonardo de Moura
|
900c56be05
|
feat(frontends/lean,library/equations_compiler): abstract proofs in equations and regular definitions
|
2017-03-25 14:22:52 -07:00 |
|
Leonardo de Moura
|
8cf43e1b30
|
feat(library/tactic/tactic_state): add tactic.run_io
|
2017-03-23 18:17:53 -07:00 |
|
Leonardo de Moura
|
fe3875a103
|
feat(library/system/io): add stdin, stdout and stderr
|
2017-03-23 16:49:39 -07:00 |
|
Leonardo de Moura
|
82748a61b7
|
feat(library/system/io): basic file system API
|
2017-03-23 16:30:16 -07:00 |
|
Leonardo de Moura
|
527c8851a8
|
refactor(library/system/io): use type classes
|
2017-03-23 14:29:07 -07:00 |
|
Gabriel Ebner
|
a8ba78e20a
|
refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic
|
2017-03-23 09:07:08 +01:00 |
|