Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
05 April 2024, 19:20:55 UTC
sort by:
Revision Author Date Message Commit Date
4a454f3 Benjamin Gregoire 03 December 2015, 10:16:56 UTC add return type when printing operator 03 December 2015, 10:16:56 UTC
4563255 Benjamin Gregoire 03 December 2015, 08:53:57 UTC allows underscore in pattern matching for fix point 03 December 2015, 08:58:44 UTC
bd34470 Pierre-Yves Strub 02 December 2015, 19:57:53 UTC `congr` handles goal of the form `P <=> Q` [fix #17275] 02 December 2015, 19:57:53 UTC
8b7c8f3 Pierre-Yves Strub 02 December 2015, 16:38:05 UTC PG keywords updated 02 December 2015, 16:38:05 UTC
693c114 Pierre-Yves Strub 02 December 2015, 16:36:54 UTC Type-checking of abbreviations. 02 December 2015, 16:36:54 UTC
5710919 Pierre-Yves Strub 02 December 2015, 16:01:34 UTC Type checking of notations. 02 December 2015, 16:01:34 UTC
9c9fe65 Pierre-Yves Strub 02 December 2015, 13:49:45 UTC Simplify BG proof :) 02 December 2015, 13:49:45 UTC
ac800ec Pierre-Yves Strub 02 December 2015, 13:40:05 UTC Remove unusable /#= rw action + add /# as a i-p. 02 December 2015, 13:44:56 UTC
7ec2538 Benjamin Gregoire 02 December 2015, 13:31:37 UTC Add lemma mkseqP 02 December 2015, 13:31:56 UTC
16caef0 Pierre-Yves Strub 02 December 2015, 11:50:03 UTC Parsing rules for notations/abbreviations. 02 December 2015, 11:50:03 UTC
d394f11 Pierre-Yves Strub 02 December 2015, 11:42:43 UTC Refactor parsing rules for operators decl/def. 02 December 2015, 11:43:07 UTC
fabbf27 Pierre-Yves Strub 02 December 2015, 09:31:57 UTC README.md: update dependencies 02 December 2015, 11:16:02 UTC
c29fc84 Benjamin Gregoire 02 December 2015, 11:14:08 UTC remove useless space in lemmas printing. 02 December 2015, 11:14:36 UTC
4be5d7a Benjamin Gregoire 02 December 2015, 11:12:57 UTC fix bug in printing of abstract theory. 02 December 2015, 11:14:36 UTC
30389e6 Pierre-Yves Strub 02 December 2015, 08:41:19 UTC Refactor op-app destructor. 02 December 2015, 09:06:31 UTC
bba28f7 Pierre-Yves Strub 02 December 2015, 08:06:17 UTC Allow the use of `_` in tuple patterns. As in: `op ['a 'b] fst (x : 'a * 'b) = let (z, _) = x in x` 02 December 2015, 09:06:31 UTC
99156b6 Benjamin Gregoire 02 December 2015, 08:18:55 UTC improve PY proof script. 02 December 2015, 08:18:55 UTC
0b16322 Benjamin Gregoire 02 December 2015, 08:12:36 UTC fixing error message for typing of module expressions. 02 December 2015, 08:13:27 UTC
e14c433 Pierre-Yves Strub 02 December 2015, 07:28:38 UTC Core fact about words. 02 December 2015, 07:28:38 UTC
36ad55c Benjamin Gregoire 01 December 2015, 21:45:59 UTC improve error messages for module application, and there localizations. 01 December 2015, 21:51:05 UTC
c4da5f6 François Dupressoir 01 December 2015, 21:02:59 UTC Removing old quantifier negations from stdlib. 01 December 2015, 21:02:59 UTC
4a65689 François Dupressoir 01 December 2015, 20:51:59 UTC NewLogic: add lemmas for negation of existentials. This is so we can stop using 'the other ones'. 01 December 2015, 20:51:59 UTC
42a4a3b François Dupressoir 01 December 2015, 20:37:28 UTC Useful lemmas on random permutations. Needs cleaning up. 01 December 2015, 20:37:28 UTC
af346b2 François Dupressoir 01 December 2015, 20:10:09 UTC PRFs and PRP-PRF switching lemma. 01 December 2015, 20:16:02 UTC
9fe4d23 François Dupressoir 01 December 2015, 15:06:29 UTC Fixing up new PRP libs and adding them back into the test suite. 01 December 2015, 20:10:56 UTC
65eda54 Pierre-Yves Strub 01 December 2015, 17:10:55 UTC Hint database for auto-exact. Add a new hint mechanism for auto-applying lemmas. Lemmas are added to the auto base with: `hint exact : L1 ... Ln.` `trivial` (and all relatives) now tries to close any goal it is presented by applying one of the lemmas of the database --- closing any generated subgoal recursively. The lemmas in the hint database are not used when `trivial` tries to close the subgoals. Lemmas are applied using a rigid unification and with the view mechanism disabled. The current implementation is linear in the size of the database. A pre-selection mechanism may be necessary in case the hint database grows too much. 01 December 2015, 17:10:55 UTC
e6a3241 Pierre-Yves Strub 01 December 2015, 15:29:19 UTC .gitignore 01 December 2015, 15:29:19 UTC
214fcfc Pierre-Yves Strub 01 December 2015, 15:16:28 UTC Pattern matching work modulo unfolding of locals. 01 December 2015, 15:19:57 UTC
a09868d Benjamin Gregoire 01 December 2015, 14:55:01 UTC improve error message: only monomorphic types are allowed 01 December 2015, 14:55:11 UTC
6829f6b Pierre-Yves Strub 01 December 2015, 14:53:47 UTC Exemplified new matching algo. 01 December 2015, 14:53:47 UTC
0db9002 Pierre-Yves Strub 01 December 2015, 14:53:33 UTC Better matching + matching always return a reduced subst. 01 December 2015, 14:53:33 UTC
7143ede Pierre-Yves Strub 01 December 2015, 13:31:21 UTC In proof-term, arguments can be partially constructed. As in: `apply (foo (x + _))` 01 December 2015, 13:31:21 UTC
3e4e3d0 Pierre-Yves Strub 01 December 2015, 12:03:49 UTC algebra: do not use t_fail internally. 01 December 2015, 12:03:49 UTC
03f2eea Pierre-Yves Strub 01 December 2015, 11:41:53 UTC More precise [proof-term checking / apply] error messages. 01 December 2015, 11:41:53 UTC
c9864c9 Pierre-Yves Strub 01 December 2015, 10:26:07 UTC nits in Number (use proof terms) 01 December 2015, 10:26:14 UTC
c12eb29 Pierre-Yves Strub 01 December 2015, 10:25:28 UTC Do not fail on non-flat unification problems. 01 December 2015, 10:26:14 UTC
be632c8 François Dupressoir 01 December 2015, 09:49:49 UTC FSet: some cleanup and extensions. 01 December 2015, 09:49:59 UTC
f184b17 François Dupressoir 01 December 2015, 09:49:35 UTC Adding info to Vagrantfile on how to set emacs up. 01 December 2015, 09:49:59 UTC
09e0145 Pierre-Yves Strub 01 December 2015, 08:39:25 UTC List: nth_rev. 01 December 2015, 08:39:25 UTC
c679271 Pierre-Yves Strub 01 December 2015, 08:26:04 UTC Importing some sha3 generic defs. 01 December 2015, 08:26:04 UTC
24322f5 Pierre-Yves Strub 30 November 2015, 14:43:56 UTC New rewrite construct: /#, /#= - /# stands for [smt ml=0] - /#= stands for [smt ml=0] + simplify. 30 November 2015, 14:43:56 UTC
6e53946 Pierre-Yves Strub 30 November 2015, 14:12:55 UTC Better check when overridding operators with type parameters. 30 November 2015, 14:12:55 UTC
81340be Pierre-Yves Strub 30 November 2015, 13:07:13 UTC Better infer. types for body of cloned operators/predicates. 30 November 2015, 13:07:13 UTC
54a39c6 Pierre-Yves Strub 30 November 2015, 11:12:48 UTC Parser/printer nits. - not bounded vars. are now printed as '_' - the syntax '_' is allowed for anonymous vars. - binders with several vars. with the same type can now be written as: `fun x y z : int => e` 30 November 2015, 11:12:48 UTC
2f59824 Pierre-Yves Strub 30 November 2015, 08:45:32 UTC Bits in BitWord + oflist/tolist. 30 November 2015, 08:45:32 UTC
4d1eabc Pierre-Yves Strub 30 November 2015, 08:23:57 UTC Import bits chunking from sha3 dev. 30 November 2015, 08:23:57 UTC
5743b3a Pierre-Yves Strub 28 November 2015, 15:00:03 UTC Nits. 28 November 2015, 15:00:03 UTC
cb30eba Pierre-Yves Strub 28 November 2015, 13:53:59 UTC List: before_find / before_index. 28 November 2015, 13:53:59 UTC
e6aedae Pierre-Yves Strub 27 November 2015, 15:39:42 UTC In formulas, give priority to prog. vars over operators. [fix #17274] 27 November 2015, 15:39:42 UTC
08837a7 Pierre-Yves Strub 27 November 2015, 10:04:30 UTC Proofs of cancelation of bs2int/int2bs. 27 November 2015, 10:04:30 UTC
795a33d Pierre-Yves Strub 26 November 2015, 19:52:10 UTC Some progress on summation. 26 November 2015, 19:52:10 UTC
cf83ecf François Dupressoir 26 November 2015, 17:02:53 UTC A first Vagrant file. This one is for use in an active version of the repository. Commented lines in the provisioning script can be used to use OPAM for everything and distribute only the Vagrantfile. TODO: Give recipes and provisioning scripts for a wider variety of archs. 26 November 2015, 17:02:53 UTC
188b473 François Dupressoir 26 November 2015, 16:02:00 UTC FSet: Some minor extensions. Need to make notations consistent throughout. 26 November 2015, 16:02:08 UTC
3dbaaf3 François Dupressoir 26 November 2015, 14:12:09 UTC NewFMap: dom_set. 26 November 2015, 16:02:08 UTC
e687477 Pierre-Yves Strub 26 November 2015, 15:37:16 UTC Nits on arithmetic && lists. 26 November 2015, 15:37:16 UTC
0f2033d Pierre-Yves Strub 25 November 2015, 15:29:24 UTC Kill all admits in RealSeq. 25 November 2015, 15:29:24 UTC
1ee53f9 Pierre-Yves Strub 25 November 2015, 15:29:13 UTC Extend Number with RealField specific results. 25 November 2015, 15:29:13 UTC
4e9daae François Dupressoir 25 November 2015, 14:38:04 UTC fix smt in DList. 25 November 2015, 14:38:26 UTC
19a83cd François Dupressoir 25 November 2015, 14:16:11 UTC fix smt in NewFMap. 25 November 2015, 14:38:26 UTC
1860966 François Dupressoir 25 November 2015, 14:07:35 UTC fix smt in List. 25 November 2015, 14:38:26 UTC
28217e7 Pierre-Yves Strub 25 November 2015, 11:11:19 UTC Progressing on countable summation, reducing all admits to ppties on limits. The lub operator has been pushed into its own theory. 25 November 2015, 11:11:19 UTC
2c0495c Pierre-Yves Strub 25 November 2015, 11:10:35 UTC More on pmap + link between map/nth/range. 25 November 2015, 11:10:35 UTC
3124db7 François Dupressoir 25 November 2015, 10:40:13 UTC Word: rewrite as a refinement of arrays. 25 November 2015, 10:57:49 UTC
4ba22d6 François Dupressoir 25 November 2015, 10:39:00 UTC NewLogic: comment out overloadings of && and ||. At the moment, the theory cannot be imported without causing issues. 25 November 2015, 10:39:00 UTC
0309ff2 François Dupressoir 25 November 2015, 10:12:14 UTC NewLogic: Equivalences of quantified statements. 25 November 2015, 10:12:32 UTC
445ce13 Benjamin Gregoire 25 November 2015, 09:27:53 UTC fix printing of lvalue in program : x[e] ---> x.[e] 25 November 2015, 09:27:53 UTC
dfdf69a Pierre-Yves Strub 24 November 2015, 21:48:29 UTC Pushing current status on real seq/series. 24 November 2015, 21:48:29 UTC
22e2b9c Pierre-Yves Strub 24 November 2015, 21:00:46 UTC Fix BitEncoding proofs. 24 November 2015, 21:01:14 UTC
323df28 François Dupressoir 24 November 2015, 20:38:59 UTC Fixing Matrix. Removing Array import from RealSeq. 24 November 2015, 20:39:38 UTC
6fe3ab2 Pierre-Yves Strub 24 November 2015, 20:05:43 UTC runtest: when in recursive mode, scan also the root directory. 24 November 2015, 20:06:03 UTC
3e2b813 François Dupressoir 24 November 2015, 16:05:42 UTC Clean Array theory. Word should be based off of this with fixed length and base type. 24 November 2015, 16:05:50 UTC
7141c60 Pierre-Yves Strub 24 November 2015, 13:36:03 UTC More results on bigops. 24 November 2015, 13:36:03 UTC
5fbe3f0 Pierre-Yves Strub 24 November 2015, 12:29:11 UTC More on divisibility and ordering. 24 November 2015, 12:29:11 UTC
a9c5810 Pierre-Yves Strub 24 November 2015, 11:36:02 UTC Start to generalize and incorporates some ad-hoc lemmas of IntDiv. 24 November 2015, 11:36:02 UTC
b8f11a3 Pierre-Yves Strub 24 November 2015, 10:28:15 UTC Integer divisibility def. + core ppties. 24 November 2015, 10:28:15 UTC
fd1b087 Pierre-Yves Strub 24 November 2015, 10:27:58 UTC Change ops. priority. Operators of the form %+(.) has the priority of \1. 24 November 2015, 10:27:58 UTC
4038b58 Pierre-Yves Strub 24 November 2015, 09:29:00 UTC More lemmas in IntDiv + notations change. Integer division is now denoted by %/ Notations priority/associativity still have to be fixed in some way. 24 November 2015, 09:29:00 UTC
9969be0 Pierre-Yves Strub 23 November 2015, 23:23:32 UTC Prune old eucliden division. Some nosmt flags may have to be removed/added. Fix stdlib. 23 November 2015, 23:23:32 UTC
1c137fc Pierre-Yves Strub 23 November 2015, 22:33:38 UTC No more axioms in IntDiv. 2 quite simple admits in Number. 23 November 2015, 22:33:38 UTC
7ed674f Pierre-Yves Strub 23 November 2015, 20:03:26 UTC Killing some admits in IntDiv. 23 November 2015, 20:03:26 UTC
ae942a2 Pierre-Yves Strub 23 November 2015, 15:30:58 UTC Start to fix admits in IntDiv. 23 November 2015, 15:30:58 UTC
1e46b0e Pierre-Yves Strub 23 November 2015, 15:04:53 UTC Yet again fixing IntDiv. 23 November 2015, 15:06:35 UTC
2797af3 Pierre-Yves Strub 23 November 2015, 11:47:14 UTC Dix def. on divz/modz. 23 November 2015, 11:47:14 UTC
44b707e Pierre-Yves Strub 23 November 2015, 11:11:40 UTC Remove some busted (admitted) results in IntDiv. 23 November 2015, 11:11:40 UTC
0f73617 Pierre-Yves Strub 23 November 2015, 09:45:16 UTC Add internal structures for match in expr/form. 23 November 2015, 09:51:56 UTC
02f8719 Pierre-Yves Strub 21 November 2015, 21:35:31 UTC When a rewrite reduces a goal to `true`, close it. This is a syntactical check (not done modulo any conversion) 21 November 2015, 21:35:31 UTC
d87e47d Pierre-Yves Strub 21 November 2015, 19:12:18 UTC `apply` in `rewrite` The syntax is `rewrite &pterm` and might change in a near future. 21 November 2015, 19:12:18 UTC
6757c4d Pierre-Yves Strub 20 November 2015, 17:48:23 UTC Some more std distributions. 20 November 2015, 17:48:23 UTC
446ac50 Pierre-Yves Strub 20 November 2015, 13:42:28 UTC # of perms (without duplicates). 20 November 2015, 13:42:28 UTC
2dff122 Pierre-Yves Strub 20 November 2015, 12:23:18 UTC Prove that we are not generating duplicates (in Perms) 20 November 2015, 12:23:18 UTC
385c46a Pierre-Yves Strub 20 November 2015, 10:18:04 UTC Generating all the permutations of a list. 20 November 2015, 10:18:36 UTC
4e6f163 Pierre-Yves Strub 19 November 2015, 15:13:55 UTC Encoding of bitstrings as integers. 19 November 2015, 15:13:55 UTC
25f1945 Pierre-Yves Strub 19 November 2015, 15:11:17 UTC Import some results on integer division. The proofs do not type-check in the stdlib and has to be fixed. These results should be derivable from IntDiv. 19 November 2015, 15:11:17 UTC
cf73075 Pierre-Yves Strub 19 November 2015, 15:10:21 UTC Core results on mkseq (List) 19 November 2015, 15:10:21 UTC
9a1feb6 Pierre-Yves Strub 19 November 2015, 15:09:58 UTC Nits in IntDiv. Still admitted results. 19 November 2015, 15:09:58 UTC
86ce178 Pierre-Yves Strub 19 November 2015, 11:41:36 UTC Rework BitWord from new Word th. 19 November 2015, 11:41:36 UTC
c31ee8a Pierre-Yves Strub 19 November 2015, 10:55:02 UTC Rework Word.eca Don't use Subtype (until this theory is stable) && use NewDistr. 19 November 2015, 10:55:16 UTC
5894d51 Pierre-Yves Strub 19 November 2015, 10:49:33 UTC Basic results on FinType. 19 November 2015, 10:49:33 UTC
33708c9 Pierre-Yves Strub 19 November 2015, 10:49:20 UTC Lossless result on standard distributions. 19 November 2015, 10:49:20 UTC
97ae7e4 Pierre-Yves Strub 19 November 2015, 10:49:07 UTC Nits in Int/List. 19 November 2015, 10:49:07 UTC
back to top