ce01988 | Adrien Koutsos | 19 June 2020, 11:54:46 UTC | allow cost precondition in rcondf, rcondt and if tactics | 19 June 2020, 11:54:46 UTC |
aac1558 | Adrien Koutsos | 12 June 2020, 15:52:02 UTC | additional simplifications of cost | 12 June 2020, 15:52:02 UTC |
92a2cd9 | Adrien Koutsos | 12 June 2020, 15:42:40 UTC | simplification of cost judgments for datatypes and tuples. | 12 June 2020, 15:43:12 UTC |
88200ac | Pierre-Yves Strub | 02 June 2020, 14:51:17 UTC | Fix cloning of user reduction (put the correct mode) | 02 June 2020, 14:51:20 UTC |
556c55d | Benjamin Gregoire | 02 June 2020, 14:50:06 UTC | small fixes | 02 June 2020, 14:50:06 UTC |
8133669 | Benjamin Gregoire | 02 June 2020, 14:16:53 UTC | small fixes | 02 June 2020, 14:16:53 UTC |
b9abebe | Pierre-Yves Strub | 02 June 2020, 14:13:38 UTC | cloning now supports schemas | 02 June 2020, 14:13:38 UTC |
8a3eafb | Pierre-Yves Strub | 28 May 2020, 07:57:19 UTC | Merge branch '1.0' into deploy-cost | 28 May 2020, 07:57:19 UTC |
3e8c6b5 | Benjamin Gregoire | 27 May 2020, 13:09:33 UTC | fix bug | 27 May 2020, 13:14:25 UTC |
6e5bd45 | Benjamin Gregoire | 27 May 2020, 13:08:56 UTC | add lemmas on bigi | 27 May 2020, 13:14:25 UTC |
6bc158c | Adrien Koutsos | 27 May 2020, 08:53:50 UTC | improved restr. printing | 27 May 2020, 08:53:50 UTC |
53ed919 | Alley Stoughton | 22 May 2020, 22:12:19 UTC | Allows nosmt with all operators other than pure, abstract ones - i.e., with plain, axiomatized (including : {t | phi} as ax) and cases operators. When cloning, [op nosmt x = ...] is allowed, but nosmt can't be used with inlining mode. | 26 May 2020, 08:38:14 UTC |
096de75 | Adrien Koutsos | 28 April 2020, 13:14:33 UTC | example of a section in the small tutorial. Also removed the debugging info when printing choare judgements. | 28 April 2020, 13:14:33 UTC |
974c7fb | Adrien Koutsos | 28 April 2020, 13:08:08 UTC | cleanup some old comments | 28 April 2020, 13:08:08 UTC |
fe1193a | Adrien Koutsos | 28 April 2020, 13:02:37 UTC | memory printing printed in a better order. | 28 April 2020, 13:02:37 UTC |
eee8d28 | Adrien Koutsos | 28 April 2020, 12:55:46 UTC | minor pretty printer improvements. | 28 April 2020, 12:55:46 UTC |
be2bf40 | Adrien Koutsos | 28 April 2020, 12:55:15 UTC | import BIA for shorter paths, + minor change. | 28 April 2020, 12:55:15 UTC |
1311f7b | Adrien Koutsos | 28 April 2020, 12:30:38 UTC | short syntax for abs. calls with invariant when there is no oracle. | 28 April 2020, 12:30:38 UTC |
b7463b6 | Adrien Koutsos | 28 April 2020, 12:01:53 UTC | Fixed shift/reduce conflicts | 28 April 2020, 12:01:53 UTC |
0ce118f | Adrien Koutsos | 28 April 2020, 11:13:08 UTC | bugs | 28 April 2020, 11:13:08 UTC |
c55ebb4 | Adrien Koutsos | 28 April 2020, 11:05:08 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-cost | 28 April 2020, 11:05:08 UTC |
170c443 | Benjamin Gregoire | 27 April 2020, 12:23:05 UTC | fix default.nix | 27 April 2020, 12:23:05 UTC |
58aaed4 | AntoineSere | 20 April 2020, 17:02:04 UTC | Merge pull request #42 from AntoineSere/eqvquo Added two useful lemmas to Quotient.ec | 20 April 2020, 17:02:04 UTC |
ce4d827 | Antoine Séré | 20 April 2020, 15:04:39 UTC | Added two useful lemmas to Quotient.ec | 20 April 2020, 15:04:39 UTC |
b8e9ba6 | Adrien Koutsos | 20 April 2020, 10:49:51 UTC | renamed files | 20 April 2020, 10:49:51 UTC |
a3cd411 | Adrien Koutsos | 16 April 2020, 15:36:20 UTC | work on FO. | 16 April 2020, 15:36:20 UTC |
acfd4ea | Pierre-Yves Strub | 16 April 2020, 14:56:46 UTC | Definition of quotient types w.r.t. a equivalence relation | 16 April 2020, 14:56:46 UTC |
60a7d34 | Pierre-Yves Strub | 16 April 2020, 13:19:34 UTC | Finite groups, cyclic groups, Bezout. | 16 April 2020, 13:19:53 UTC |
cdb2e6f | François Dupressoir | 16 April 2020, 10:45:54 UTC | Use arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '=' | 16 April 2020, 10:45:54 UTC |
f44260c | Pierre-Yves Strub | 16 April 2020, 09:41:06 UTC | stdlib: distributions: dmap1E_can | 16 April 2020, 09:41:06 UTC |
94786bc | Pierre-Yves Strub | 16 April 2020, 09:40:44 UTC | stdlib: List: nth_default | 16 April 2020, 09:40:44 UTC |
136b237 | Pierre-Yves Strub | 15 April 2020, 09:39:30 UTC | lemma: fun_ext2 | 15 April 2020, 09:39:30 UTC |
5eba66b | Pierre-Yves Strub | 15 April 2020, 09:31:23 UTC | allow writing m.[i, j] in place of m.[(i, j)] | 15 April 2020, 09:31:23 UTC |
4882379 | Pierre-Yves Strub | 15 April 2020, 08:28:48 UTC | views: allow application of induction principle as a view | 15 April 2020, 08:28:48 UTC |
64d592d | Pierre-Yves Strub | 15 April 2020, 08:19:44 UTC | elim: search quantifier modulo reduction | 15 April 2020, 08:19:54 UTC |
3b8b038 | Adrien Koutsos | 14 April 2020, 15:08:58 UTC | Fixed unclosed box. (#41) Co-authored-by: Adrien Koutsos <akoutsos@users.noreply.github.com> | 14 April 2020, 15:08:58 UTC |
56b5594 | Adrien Koutsos | 14 April 2020, 14:27:28 UTC | FO | 14 April 2020, 14:28:52 UTC |
f3581d5 | Pierre-Yves Strub | 10 April 2020, 09:56:42 UTC | binomial coefficients | 10 April 2020, 09:56:42 UTC |
eb9b026 | Pierre-Yves Strub | 09 April 2020, 16:21:20 UTC | CI: move to slack notification | 09 April 2020, 16:22:07 UTC |
21e8fce | Pierre-Yves Strub | 09 April 2020, 16:21:20 UTC | CI: move to slack notification | 09 April 2020, 16:21:20 UTC |
ffe2fd6 | Adrien Koutsos | 09 April 2020, 14:45:34 UTC | Matching issue | 09 April 2020, 14:45:34 UTC |
d41a34d | Pierre-Yves Strub | 09 April 2020, 13:43:45 UTC | Matching for *hoareF & Pr | 09 April 2020, 13:44:05 UTC |
4062085 | bgregoir | 09 April 2020, 13:39:11 UTC | Merge pull request #40 from CohenCyril/nixfix default.nix: adding installFlags | 09 April 2020, 13:39:11 UTC |
ad74e06 | Adrien Koutsos | 09 April 2020, 12:24:40 UTC | minor printing change | 09 April 2020, 12:24:40 UTC |
cb5a4f9 | Adrien Koutsos | 09 April 2020, 12:22:30 UTC | fixed BR example. | 09 April 2020, 12:22:30 UTC |
1eca4b1 | Adrien Koutsos | 09 April 2020, 11:52:57 UTC | Proof obligation generated only if necessary + error message. | 09 April 2020, 11:52:57 UTC |
39d94f3 | Adrien Koutsos | 09 April 2020, 10:44:27 UTC | bug fix for free variables and pretty printing. | 09 April 2020, 10:44:27 UTC |
e0898d5 | Adrien Koutsos | 09 April 2020, 08:58:38 UTC | bug fix | 09 April 2020, 08:58:38 UTC |
589e509 | Adrien Koutsos | 09 April 2020, 08:30:25 UTC | splitted proof obligations | 09 April 2020, 08:30:25 UTC |
2fd58e3 | Adrien Koutsos | 09 April 2020, 08:30:09 UTC | Matching for choaref | 09 April 2020, 08:30:09 UTC |
75af940 | Pierre-Yves Strub | 08 April 2020, 13:58:49 UTC | matching for Pr | 09 April 2020, 08:08:11 UTC |
a9eb399 | Pierre-Yves Strub | 08 April 2020, 13:50:35 UTC | matching for *hoareF | 09 April 2020, 08:08:11 UTC |
21354f7 | Cyril Cohen | 08 April 2020, 15:21:04 UTC | default.nix: adding installFlags | 08 April 2020, 15:23:25 UTC |
c331657 | Adrien Koutsos | 08 April 2020, 15:20:57 UTC | cleanup | 08 April 2020, 15:20:57 UTC |
9c85231 | Adrien Koutsos | 08 April 2020, 13:03:17 UTC | examples changes | 08 April 2020, 13:03:17 UTC |
daeacbd | Adrien Koutsos | 08 April 2020, 11:45:55 UTC | Alternative simpler syntax for cost judgement with true ==> true. | 08 April 2020, 11:45:55 UTC |
35475fa | Adrien Koutsos | 08 April 2020, 11:04:05 UTC | Bug fx + updated examples. | 08 April 2020, 11:04:05 UTC |
87273a4 | Adrien Koutsos | 08 April 2020, 10:37:25 UTC | printing improvement | 08 April 2020, 10:37:25 UTC |
952baf6 | Adrien Koutsos | 07 April 2020, 15:54:32 UTC | Apply on module with restrictions. | 07 April 2020, 15:54:32 UTC |
0e73f5c | Adrien Koutsos | 07 April 2020, 10:31:37 UTC | Proof obligation when applying a forall on a restricted module. | 07 April 2020, 10:31:37 UTC |
4193812 | Adrien Koutsos | 06 April 2020, 16:18:19 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-cost | 06 April 2020, 16:18:19 UTC |
149b09f | Pierre-Yves Strub | 28 March 2020, 08:13:02 UTC | User error message for map-style lvalue on unsupported assignment [fix #17412] | 28 March 2020, 08:13:21 UTC |
b1b35e6 | Pierre-Yves Strub | 26 March 2020, 19:52:54 UTC | Internal: remove LvMap lvalue. | 26 March 2020, 19:52:54 UTC |
1a8d60a | Pierre-Yves Strub | 26 March 2020, 18:26:21 UTC | Revert "better conversion + simplify reduction algorithm." This reverts commit 11a875951d0f94381b22b362ddf8b0cc18f77886. | 26 March 2020, 18:26:21 UTC |
ea602f8 | Adrien Koutsos | 26 March 2020, 16:40:42 UTC | Changed oracle restrictions in module type. Default to zero. | 26 March 2020, 16:40:42 UTC |
2a5b4f6 | Pierre-Yves Strub | 26 March 2020, 07:42:17 UTC | Only accepts Alt-Ergo from version 2.3.1 | 26 March 2020, 07:42:17 UTC |
098adb2 | Adrien Koutsos | 25 March 2020, 09:09:46 UTC | Fix previous merge | 25 March 2020, 09:09:46 UTC |
ab9b383 | Adrien Koutsos | 24 March 2020, 17:45:32 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-cost | 24 March 2020, 17:45:32 UTC |
c5c3324 | Adrien Koutsos | 24 March 2020, 14:20:23 UTC | instantiation rule for choare judgement | 24 March 2020, 14:20:23 UTC |
285fdb7 | Adrien Koutsos | 23 March 2020, 17:07:05 UTC | started implementing choare instantiation rule | 23 March 2020, 17:07:05 UTC |
e7dfa75 | Adrien Koutsos | 23 March 2020, 15:21:01 UTC | progress for choare judgement: remains to update apply | 23 March 2020, 15:21:01 UTC |
99a37b4 | Adrien Koutsos | 23 March 2020, 15:20:37 UTC | decreasing quantity in while tactic: cost.ec fix | 23 March 2020, 15:20:37 UTC |
61ef975 | Adrien Koutsos | 23 March 2020, 14:12:14 UTC | choare are only for abstract calls. | 23 March 2020, 14:12:14 UTC |
fa4d0e4 | Adrien Koutsos | 23 March 2020, 09:01:10 UTC | small cleanup | 23 March 2020, 09:01:10 UTC |
29fd288 | Adrien Koutsos | 19 March 2020, 17:02:04 UTC | Correct parsing of memory restrictions. | 19 March 2020, 17:02:04 UTC |
9bc4cf8 | Adrien Koutsos | 19 March 2020, 16:45:59 UTC | Bug fix, empty restrictions were not properly handled. | 19 March 2020, 16:45:59 UTC |
3601773 | Adrien Koutsos | 19 March 2020, 16:30:59 UTC | while with decreasing quantity | 19 March 2020, 16:30:59 UTC |
f3b1f7f | Adrien Koutsos | 19 March 2020, 15:59:54 UTC | Small precision improvement. Added the invariant to the cost of while loop conditions | 19 March 2020, 15:59:54 UTC |
79619e4 | Adrien Koutsos | 19 March 2020, 15:56:34 UTC | Rnd tactic fix: lossless precondition was forgotten. | 19 March 2020, 15:57:37 UTC |
928a0fa | Adrien Koutsos | 19 March 2020, 15:45:56 UTC | use max for cost of if statements | 19 March 2020, 15:45:56 UTC |
7f9f6f8 | Adrien Koutsos | 19 March 2020, 15:06:49 UTC | Minor | 19 March 2020, 15:06:49 UTC |
0106a13 | Adrien Koutsos | 18 March 2020, 12:58:39 UTC | small parser improvement + bug fix | 18 March 2020, 12:58:39 UTC |
b694564 | Adrien Koutsos | 18 March 2020, 11:40:29 UTC | parser bug fix + updated examples. | 18 March 2020, 11:40:29 UTC |
aaf4070 | Adrien Koutsos | 18 March 2020, 11:32:24 UTC | Added memory predicate variables in schemata | 18 March 2020, 11:32:24 UTC |
e182b0c | Adrien Koutsos | 17 March 2020, 17:33:24 UTC | Adding memory predicate variables in schemata + better reduce_user | 17 March 2020, 17:33:24 UTC |
980d84b | Adrien Koutsos | 17 March 2020, 12:17:23 UTC | Bug fix. | 17 March 2020, 12:17:23 UTC |
f9c15b9 | Adrien Koutsos | 17 March 2020, 11:50:46 UTC | examples + br93 done + small fix in while tactic. | 17 March 2020, 11:50:46 UTC |
309e263 | Benjamin Gregoire | 16 March 2020, 18:13:28 UTC | find as while | 16 March 2020, 18:13:28 UTC |
b0f81e3 | Adrien Koutsos | 16 March 2020, 15:01:02 UTC | started replacing the list by a while. | 16 March 2020, 15:01:02 UTC |
cbab513 | Adrien Koutsos | 16 March 2020, 13:24:18 UTC | Added an optional precondition to the wp tactic. | 16 March 2020, 13:24:18 UTC |
9127e98 | Adrien Koutsos | 16 March 2020, 09:08:58 UTC | Revert "To be reverted." This reverts commit c12ce5a9d6a461c2345f2cd76aaf676d1a6ea4e3. | 16 March 2020, 09:08:58 UTC |
22799f1 | Pierre-Yves Strub | 28 February 2020, 06:49:27 UTC | In `rewrite`, use a keyed matching algorithm for finding occurences. | 28 February 2020, 06:49:27 UTC |
c12ce5a | Adrien Koutsos | 27 February 2020, 13:18:44 UTC | To be reverted. | 27 February 2020, 13:18:44 UTC |
ad1aa95 | Adrien Koutsos | 26 February 2020, 18:23:24 UTC | Minor | 26 February 2020, 18:23:24 UTC |
ad8432b | Adrien Koutsos | 26 February 2020, 17:26:13 UTC | Can use hint simplify with schema containing costs. Note that this is somehow limited (no matching in cost judgements' precondition). | 26 February 2020, 17:26:13 UTC |
c28125a | Adrien Koutsos | 26 February 2020, 14:31:32 UTC | Corrected a bug with schema instantiations. Expression variable in cost judgemement's preconditions were not substituted. | 26 February 2020, 14:31:32 UTC |
38e6067 | Adrien Koutsos | 26 February 2020, 14:30:37 UTC | Printing improvement. | 26 February 2020, 14:30:37 UTC |
f9ad123 | Adrien Koutsos | 25 February 2020, 18:07:51 UTC | Simplify automatically free costs. | 25 February 2020, 18:07:51 UTC |
71fded7 | Adrien Koutsos | 25 February 2020, 14:26:12 UTC | Various bugfix. | 25 February 2020, 14:26:12 UTC |
8b59df9 | Adrien Koutsos | 20 February 2020, 17:18:16 UTC | Fleshing out the BR93 example. | 20 February 2020, 17:18:16 UTC |