https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
9f6a2f9 add make 07 July 2016, 06:32:45 UTC
776af38 Why3: => 0.87 06 July 2016, 20:52:42 UTC
f3ba127 Better parsing of mdistr types. 12 January 2016, 09:43:08 UTC
f007c3f Nits in IntDiv. 10 January 2016, 11:50:00 UTC
d42f414 Uniform distribution on words: Splitting uniformity and fullness. 08 January 2016, 20:22:16 UTC
0f42e50 small fix 08 January 2016, 12:04:40 UTC
f026337 Uniform distributions are uniform. 08 January 2016, 03:49:29 UTC
da610f0 do not remove whitespaces (.dir-locals) - PG mode is buggy on that 08 January 2016, 03:46:38 UTC
fbd222b Refactoring a bit Vagrantfile. 05 January 2016, 21:59:08 UTC
352f5cc remove trailing whitespaces 04 January 2016, 14:57:38 UTC
00622b9 emacs local variables for trailing whitespaces removal. 04 January 2016, 14:57:20 UTC
8ae369b license: do not create trailing whitespaces 04 January 2016, 14:57:12 UTC
675c6bd small improvement 04 January 2016, 14:26:55 UTC
1d1f362 COPYRIGHT (2016 / headers) 03 January 2016, 10:13:41 UTC
6b8e0e2 COPYRIGHT (2016) 03 January 2016, 10:13:19 UTC
8133719 Variant of `case` that retains the case equation. Syntax is `case _: ...`, and work as in vanilla variant, but retains the case equation (that is pushed as a top-assumption). 03 January 2016, 10:12:30 UTC
0e9c8b6 replug + generalize the tactic exists* to any expression. 03 January 2016, 10:10:03 UTC
0546b4a minor changes 18 December 2015, 20:59:41 UTC
0bf18f8 minor changes. 18 December 2015, 20:59:40 UTC
0b95d24 NewDistr: extending standard distributions with support lemmas. 18 December 2015, 20:59:40 UTC
7c79378 PG keywords updated 18 December 2015, 20:59:28 UTC
f0d849f add lemmas in the sodlib 18 December 2015, 08:13:07 UTC
98986d8 add more possibilities to change the bound in phoare 18 December 2015, 08:13:06 UTC
06d13a5 Nits in Lists (cleaning a bit + some basic results) 17 December 2015, 21:04:13 UTC
4ea99e2 remove some debugging printf 17 December 2015, 20:26:15 UTC
51c94f5 print the goal by default in error message for apply + small modification of the formatting 17 December 2015, 19:55:01 UTC
b784ecd In `phl` tactics, display the goal when an internal `apply` failed. 17 December 2015, 16:18:01 UTC
7f2bfa9 Move HiGoal.LowApply to LowGoal.Apply + make use of the hi/low-apply in phl tactics 17 December 2015, 16:10:56 UTC
ddd9e62 one more time Francois ... 17 December 2015, 15:57:36 UTC
c95a61f Start playing a bit with `hint exact` in the stdlib. 16 December 2015, 18:31:22 UTC
062d0f8 `exact` hints can be declared local. Such hints are not imported. 16 December 2015, 18:31:21 UTC
28d74f3 Code style (.ec) 16 December 2015, 18:31:19 UTC
8ab78bb Fix `[*]` i-p that was doing some delta. 16 December 2015, 18:10:20 UTC
04743fa Fold version of oracle looping. 16 December 2015, 18:10:19 UTC
f4b94e8 Implement ssr compatible naming for i-p. - `move=> _` does a late clear - `move=> ?` does an anonymous (_) intro This is currently not enabled by default. The option `oldip` has first to be cleared (`pragma -oldip`) 16 December 2015, 18:07:43 UTC
65269da Internals: ax_spec is no more a `form option` 16 December 2015, 17:25:53 UTC
d378204 Some cleaning on IterProc. 16 December 2015, 17:10:37 UTC
a722c7a ambient `auto`: do not fail on first non-applicable lemma in the db. Really... 16 December 2015, 16:17:42 UTC
62ee9c8 ambient `auto`: do not fail on first non-applicable lemma in the db. 16 December 2015, 16:02:36 UTC
46901a7 New syntax for equiv. eq: `={| f1, ..., fn |}`. This syntax is a notation for `f1{1} = f1{2} /\ ...` [close #17284] 16 December 2015, 15:31:38 UTC
0b4bb01 Refactor theory replay in its own module. 16 December 2015, 12:00:36 UTC
8f6c385 Refactoring hi-cloning into smaller functions. 16 December 2015, 10:06:49 UTC
62ee2cc Refactoring .mli 15 December 2015, 14:30:07 UTC
b20b595 set default value max_lemmas to 0 when wanted_lemmas is given 15 December 2015, 12:43:27 UTC
18353b9 A bit more on chunking. 15 December 2015, 11:40:22 UTC
3262b68 Generic reasoning about procedure iteration. 15 December 2015, 11:40:21 UTC
6065048 Making transpose an abbreviation. Also reworking a proof in Rel to make it fit in 80 chars. 15 December 2015, 11:40:20 UTC
7c1e7b7 Parse only notations. Notation can be declared parse-only via the option `printing`, as in: `abbrev [-printing] succ (x : int) = x` [close #17280] 15 December 2015, 08:45:06 UTC
b02e4e4 Factor out notations typing. 15 December 2015, 08:45:06 UTC
f83acc1 improve eager: eager proc works on abstract functions. 15 December 2015, 08:45:05 UTC
75174e7 generalize lemma ... 15 December 2015, 07:09:38 UTC
0901c4f New occurence selector: `{+}`. Select all occurences. Allow to not clear generalized variables, using: `move: {+}x` (~ to `move: (x)`). 14 December 2015, 19:43:55 UTC
f65f5f1 Post-tactic generalize. Syntax is `tactic <@ foo`. Can be mixed with `tactic=> ...`. 14 December 2015, 17:07:28 UTC
06a078f Allows chaining '=> ...' Subsequent `=> ...` do not perform a case-analysis by default. 14 December 2015, 16:05:19 UTC
55a997a Simplification i-p/rw that do not break the product compatibility. Syntax is `/~=` && `//~=` (with done) 14 December 2015, 15:26:36 UTC
58337f0 Do not clear local hyps when generalized as-is. 14 December 2015, 14:23:31 UTC
7476fe1 Removing internal implem. of removed `move=> x!` 14 December 2015, 12:02:26 UTC
65f95ac Intro-pattern: `n!->` (n optional, `->` can be `<-`) Repeat `->` at most `n` times. 14 December 2015, 11:59:14 UTC
108a489 Removing (from parser) intro-patterm `x!` (unused) 14 December 2015, 11:59:14 UTC
f61598c Lexems `<-`, `->`, `<<-`, `->>` can now be glued together. 14 December 2015, 11:38:46 UTC
53b710e Predicates on relations from SSR. transpose should be made a parse-only notation 14 December 2015, 11:38:45 UTC
49d4ab8 Lists: subseq + more on sorts. Some admits in subseq. 14 December 2015, 10:13:47 UTC
3aa90e0 generalize lemma 14 December 2015, 10:13:46 UTC
b690a3b IntDiv: nits. 13 December 2015, 19:19:00 UTC
1e48f0a New intro-pattern: `<*>` This intro-pattern applies `subst` on all the top-assumptions. It is possible to restrict the construct to exactly `n` top-assumptions by rewriting `n!<*>`. Top-assumptions that have been substituted are cleared, other ones are kept untouched. 13 December 2015, 14:16:19 UTC
b7ffa02 Syntax change: `[n*]` -> `[n!*]` 13 December 2015, 14:16:18 UTC
4388214 I-p `[*]` can now do case analysis of ind. pred. ~ to `and`. Syntax is `[~*]`. The full syntax of this i-p is now: `move=> [int?~?/?*]` 12 December 2015, 20:03:33 UTC
c09a98a I-p `[*]` can now delta-unfold on demande. The syntax is `[/*]`. The full syntax of this intro-pattern is now: `move=> [int?/?*]` 12 December 2015, 11:55:17 UTC
49ccbc4 Intro-pattern `[!*]`. Same as `[*]`, but destruct all top-assumptions. 12 December 2015, 11:55:16 UTC
95d9ef9 Intro-pattern `[*]` do not delta-unfold top-assumptions. 12 December 2015, 11:55:14 UTC
2763987 Intro-pattern `[*]` fully destruct all the top-ands of the top-assumption. The variant `[n*]` do the same-process on the `n` first top-assumptions. 12 December 2015, 10:38:44 UTC
e188bb2 t_left -> t_right. 11 December 2015, 19:30:09 UTC
055f122 `left` / `right` now handles ind. pred. ~ to or. 11 December 2015, 18:18:17 UTC
a8d79e1 `split` now handles ind. pred. ~ to and. 11 December 2015, 18:18:16 UTC
c37c760 Check for duplicated constructor names in ind. pred. 11 December 2015, 18:18:15 UTC
a53f58b Ind. pr. intro lemmas have the name of their respective ctr. 11 December 2015, 18:18:14 UTC
2cccc61 `case` tactic now works on inductive predicates. 11 December 2015, 18:18:13 UTC
a9c3b6b PRP<->PRF-like lemma when the adversary can query the inverse permutation oracle. 11 December 2015, 14:46:45 UTC
cc8ba00 Do not use `felsum` op. anymore. 11 December 2015, 14:39:15 UTC
6154aaa Ind. predicate are now equipped with their intro/elim schemes. 11 December 2015, 14:10:53 UTC
2a41e40 In BitWord, inline `card` (with 2) 11 December 2015, 14:09:05 UTC
6440e8d add trivial lemma 11 December 2015, 14:09:04 UTC
fc23436 improve lemma rng_set 11 December 2015, 12:00:26 UTC
96ce566 Inductive (non-rec) pred. parsing + typing. 11 December 2015, 11:59:59 UTC
f95613d Factorize out predicates related typing functions. 11 December 2015, 11:56:34 UTC
a09fa95 add lemmas 11 December 2015, 09:51:20 UTC
405f7dd Do not complain about goal count mismatch on `[]`. 10 December 2015, 15:17:13 UTC
b3066c4 `case` && `elim` now takes clear genpattern + views (for `case`). 10 December 2015, 15:05:56 UTC
cdb1f75 Remove duplicated abbrev. for (-) in RealOrder. 10 December 2015, 13:03:49 UTC
13b6eeb PG: new var.: easycrypt-prog-args 10 December 2015, 12:16:13 UTC
bddc0d5 Categorize `rewrite` as a case-like tactic. This means that if the first i-p (pruning simplication ones) is a `case` i-p, no case analysis is done. Previous behaviour can be recovered by prepending a `-` (i.e. by flusing the i-p chain) Scripts can be updated with: gsed -i 's@rewrite\([^;]*=>\( */=\)\?\) *\[@rewrite\1 -[@g' **/*.ec* 10 December 2015, 09:21:58 UTC
a820b13 Remove `intro` Scripts can be updated with: gsed -i 's/intros *\(=>\)\? */move=> /g' **/*.ec* 10 December 2015, 09:21:50 UTC
243c3ba Remove `generalize` Scripts should now use `move: `. Use `gsed -i 's/generalize */move: /g' **/*.ec*` to update scripts. 10 December 2015, 09:21:41 UTC
1e62fd9 In stdlib, don't assume that rewrite in a non-case tactic. 10 December 2015, 09:21:32 UTC
2fed99d In stdlib, don't use `intros` anymore 10 December 2015, 09:20:33 UTC
9f8880d In stdlib, don't use `generalize` anymore 10 December 2015, 09:20:24 UTC
6937ece In pp: priority of uniry arith ops. have a priority equal to their binary counter-parts. This is in accordance with the parser definition. As a consequence, when mixing [-]/[+] with (-)/(+), the pp now prints explicit parentheses in all cases. Given the unusual precedences unary operators have, we should stick to this until we fix them. 09 December 2015, 19:30:13 UTC
92900c9 Crude detection of identity rewriting. The mechanism is to forbid non-keyed matching in `rewrite` when LHS && RHS of the rewriting equation are convertible. Currently, the whole `rewrite` is rejected if the matching succeeds but the result would result in a identity rewriting. A better mechanism should embed the identity detection rewriting mechanism into the form matching one. 09 December 2015, 16:49:49 UTC
b3f11a9 Add 'eta-reduction'. 09 December 2015, 15:51:09 UTC
0fa2523 Fix pretty-printer w.r.t. operators' priorities. [fix #17276] 09 December 2015, 15:34:08 UTC
back to top