| 7a77090 | Pierre-Yves Strub | 02 December 2015, 07:28:38 UTC | Core fact about words. | 02 December 2015, 07:28:46 UTC |
| 90ece64 | Benjamin Gregoire | 01 December 2015, 21:45:59 UTC | improve error messages for module application, and there localizations. | 01 December 2015, 21:55:03 UTC |
| cc67710 | François Dupressoir | 01 December 2015, 21:02:59 UTC | Removing old quantifier negations from stdlib. | 01 December 2015, 21:12:10 UTC |
| 91a1969 | 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, 21:12:09 UTC |
| 8f229a1 | François Dupressoir | 01 December 2015, 20:37:28 UTC | Useful lemmas on random permutations. Needs cleaning up. | 01 December 2015, 21:12:08 UTC |
| 3915c77 | François Dupressoir | 01 December 2015, 20:10:09 UTC | PRFs and PRP-PRF switching lemma. | 01 December 2015, 21:12:07 UTC |
| 1de78d7 | 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, 21:12:06 UTC |
| 2998c27 | 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:29:46 UTC |
| 7cc81de | Pierre-Yves Strub | 01 December 2015, 15:29:19 UTC | .gitignore | 01 December 2015, 15:29:30 UTC |
| e1b70b4 | Pierre-Yves Strub | 01 December 2015, 15:16:28 UTC | Pattern matching work modulo unfolding of locals. | 01 December 2015, 15:27:06 UTC |
| 1731c7e | Benjamin Gregoire | 01 December 2015, 14:55:01 UTC | improve error message: only monomorphic types are allowedt | 01 December 2015, 14:57:45 UTC |
| ecaaf69 | Pierre-Yves Strub | 01 December 2015, 14:53:47 UTC | Exemplified new matching algo. | 01 December 2015, 14:54:52 UTC |
| 95a4b45 | Pierre-Yves Strub | 01 December 2015, 14:53:33 UTC | Better matching + matching always return a reduced subst. | 01 December 2015, 14:54:45 UTC |
| df925d2 | 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:40 UTC |
| 0fcb523 | Pierre-Yves Strub | 01 December 2015, 12:03:49 UTC | algebra: do not use t_fail internally. | 01 December 2015, 12:03:59 UTC |
| f8aee22 | Pierre-Yves Strub | 01 December 2015, 11:50:02 UTC | More precise [proof-term checking / apply] error messages. | 01 December 2015, 11:50:02 UTC |
| b9ff6ff | Pierre-Yves Strub | 01 December 2015, 10:26:07 UTC | nits in Number (use proof terms) | 01 December 2015, 10:26:29 UTC |
| e15bc1d | Pierre-Yves Strub | 01 December 2015, 10:25:28 UTC | Do not fail on non-flat unification problems. | 01 December 2015, 10:26:29 UTC |
| 9d31264 | François Dupressoir | 01 December 2015, 09:49:49 UTC | FSet: some cleanup and extensions. | 01 December 2015, 10:26:28 UTC |
| 95b5ca7 | François Dupressoir | 01 December 2015, 09:49:35 UTC | Adding info to Vagrantfile on how to set emacs up. | 01 December 2015, 10:26:27 UTC |
| 2044e32 | Pierre-Yves Strub | 01 December 2015, 08:39:25 UTC | List: nth_rev. | 01 December 2015, 08:40:30 UTC |
| a12953c | Pierre-Yves Strub | 01 December 2015, 08:26:04 UTC | Importing some sha3 generic defs. | 01 December 2015, 08:26:51 UTC |
| a0b80ad | 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:45:33 UTC |
| ccd708f | Pierre-Yves Strub | 30 November 2015, 14:12:55 UTC | Better check when overridding operators with type parameters. | 30 November 2015, 14:13:03 UTC |
| b1404f2 | Pierre-Yves Strub | 30 November 2015, 13:07:13 UTC | Better infer. types for body of cloned operators/predicates. | 30 November 2015, 13:07:31 UTC |
| 9843498 | 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:19:09 UTC |
| 0a4653f | Pierre-Yves Strub | 30 November 2015, 08:45:32 UTC | Bits in BitWord + oflist/tolist. | 30 November 2015, 08:46:31 UTC |
| c4f2b14 | Pierre-Yves Strub | 30 November 2015, 08:23:57 UTC | Import bits chunking from sha3 dev. | 30 November 2015, 08:24:10 UTC |
| 24c586c | Pierre-Yves Strub | 28 November 2015, 15:00:03 UTC | Nits. | 28 November 2015, 15:00:15 UTC |
| 0e96fcf | Pierre-Yves Strub | 28 November 2015, 13:53:59 UTC | List: before_find / before_index. | 28 November 2015, 13:54:08 UTC |
| 67c363e | Pierre-Yves Strub | 27 November 2015, 15:39:42 UTC | In formulas, give priority to prog. vars over operators. | 27 November 2015, 15:40:00 UTC |
| ace7b84 | Pierre-Yves Strub | 27 November 2015, 13:55:39 UTC | Replug `transitivity` | 27 November 2015, 13:55:39 UTC |
| cfccd98 | Pierre-Yves Strub | 27 November 2015, 10:04:30 UTC | Proofs of cancelation of bs2int/int2bs. | 27 November 2015, 10:04:38 UTC |
| d31699b | Pierre-Yves Strub | 26 November 2015, 19:52:10 UTC | Some progress on summation. | 26 November 2015, 19:52:20 UTC |
| e468348 | 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, 19:44:01 UTC |
| b2e73f6 | François Dupressoir | 26 November 2015, 16:02:00 UTC | FSet: Some minor extensions. Need to make notations consistent throughout. | 26 November 2015, 19:44:00 UTC |
| f67e461 | François Dupressoir | 26 November 2015, 14:12:09 UTC | NewFMap: dom_set. | 26 November 2015, 19:43:58 UTC |
| 560f448 | Pierre-Yves Strub | 26 November 2015, 15:37:16 UTC | Nits on arithmetic && lists. | 26 November 2015, 15:37:55 UTC |
| d05a093 | Pierre-Yves Strub | 25 November 2015, 15:29:24 UTC | Kill all admits in RealSeq. | 25 November 2015, 15:29:35 UTC |
| edccc8b | Pierre-Yves Strub | 25 November 2015, 15:29:13 UTC | Extend Number with RealField specific results. | 25 November 2015, 15:29:34 UTC |
| f3fb324 | François Dupressoir | 25 November 2015, 14:38:04 UTC | fix smt in DList. | 25 November 2015, 14:40:56 UTC |
| 75690fb | François Dupressoir | 25 November 2015, 14:16:11 UTC | fix smt in NewFMap. | 25 November 2015, 14:40:55 UTC |
| e4dd849 | François Dupressoir | 25 November 2015, 14:07:35 UTC | fix smt in List. | 25 November 2015, 14:40:52 UTC |
| 098dfb0 | 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:30 UTC |
| ffe0d4f | Pierre-Yves Strub | 25 November 2015, 11:10:35 UTC | More on pmap + link between map/nth/range. | 25 November 2015, 11:11:29 UTC |
| 5bc7419 | François Dupressoir | 25 November 2015, 10:40:13 UTC | Word: rewrite as a refinement of arrays. | 25 November 2015, 11:06:55 UTC |
| ec412c2 | 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, 11:06:54 UTC |
| 8f4435c | François Dupressoir | 25 November 2015, 10:12:14 UTC | NewLogic: Equivalences of quantified statements. | 25 November 2015, 10:14:40 UTC |
| b57d8a5 | Benjamin Gregoire | 25 November 2015, 09:27:53 UTC | fix printing of lvalue in program : x[e] ---> x.[e] | 25 November 2015, 09:45:22 UTC |
| b57ee16 | Pierre-Yves Strub | 24 November 2015, 21:48:29 UTC | Pushing current status on real seq/series. | 24 November 2015, 21:48:38 UTC |
| dc6856e | Pierre-Yves Strub | 24 November 2015, 21:00:46 UTC | Fix BitEncoding proofs. | 24 November 2015, 21:01:36 UTC |
| d25415a | François Dupressoir | 24 November 2015, 20:38:59 UTC | Fixing Matrix. Removing Array import from RealSeq. | 24 November 2015, 21:01:35 UTC |
| 9b3d27b | 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, 20:06:23 UTC |
| a334b84 | 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:20 UTC |
| e73c89e | Pierre-Yves Strub | 24 November 2015, 13:36:03 UTC | More results on bigops. | 24 November 2015, 13:36:26 UTC |
| b953aef | Benjamin Gregoire | 24 November 2015, 12:50:08 UTC | fix syntax | 24 November 2015, 12:50:08 UTC |
| 6623704 | Pierre-Yves Strub | 24 November 2015, 12:29:11 UTC | More on divisibility and ordering. | 24 November 2015, 12:29:36 UTC |
| d6c87af | 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:19 UTC |
| b0dffaf | Pierre-Yves Strub | 24 November 2015, 10:28:15 UTC | Integer divisibility def. + core ppties. | 24 November 2015, 10:28:35 UTC |
| d9d5e00 | 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:28:34 UTC |
| 6dcc4e0 | 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:27 UTC |
| 07688b7 | 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. | 24 November 2015, 09:29:26 UTC |
| cca705e | 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:34:18 UTC |
| 1d114d8 | Pierre-Yves Strub | 23 November 2015, 20:03:26 UTC | Killing some admits in IntDiv. | 23 November 2015, 22:34:17 UTC |
| 1c0b2d9 | Pierre-Yves Strub | 23 November 2015, 15:30:58 UTC | Start to fix admits in IntDiv. | 23 November 2015, 22:34:16 UTC |
| 020ace6 | Pierre-Yves Strub | 23 November 2015, 15:04:53 UTC | Yet again fixing IntDiv. | 23 November 2015, 22:34:15 UTC |
| 6b674da | Pierre-Yves Strub | 23 November 2015, 11:47:14 UTC | Dix def. on divz/modz. | 23 November 2015, 11:47:47 UTC |
| efad303 | Pierre-Yves Strub | 23 November 2015, 11:11:40 UTC | Remove some busted (admitted) results in IntDiv. | 23 November 2015, 11:11:55 UTC |
| ad6c299 | Pierre-Yves Strub | 23 November 2015, 09:45:16 UTC | Add internal structures for match in expr/form. | 23 November 2015, 09:51:40 UTC |
| d2ea2ab | 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:36:49 UTC |
| 7a12e71 | 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:44 UTC |
| b0300a9 | Pierre-Yves Strub | 20 November 2015, 17:48:23 UTC | Some more std distributions. | 21 November 2015, 19:12:38 UTC |
| 1ea5fe4 | Pierre-Yves Strub | 20 November 2015, 13:42:28 UTC | # of perms (without duplicates). | 20 November 2015, 13:43:39 UTC |
| 01407ef | Pierre-Yves Strub | 20 November 2015, 12:23:18 UTC | Prove that we are not generating duplicates (in Perms) | 20 November 2015, 13:43:38 UTC |
| d7b8fdb | Pierre-Yves Strub | 20 November 2015, 10:18:04 UTC | Generating all the permutations of a list. | 20 November 2015, 13:43:34 UTC |
| 3dc3e59 | Pierre-Yves Strub | 19 November 2015, 15:13:55 UTC | Encoding of bitstrings as integers. | 19 November 2015, 15:14:34 UTC |
| 839c366 | 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:14:34 UTC |
| 27cecfd | Pierre-Yves Strub | 19 November 2015, 15:10:21 UTC | Core results on mkseq (List) | 19 November 2015, 15:14:33 UTC |
| c764cd3 | Pierre-Yves Strub | 19 November 2015, 15:09:58 UTC | Nits in IntDiv. Still admitted results. | 19 November 2015, 15:14:32 UTC |
| 46d475e | Pierre-Yves Strub | 19 November 2015, 11:41:36 UTC | Rework BitWord from new Word th. | 19 November 2015, 11:41:58 UTC |
| 35eebc6 | 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:56:07 UTC |
| e07964c | Pierre-Yves Strub | 19 November 2015, 10:49:33 UTC | Basic results on FinType. | 19 November 2015, 10:56:07 UTC |
| 7b9ab08 | Pierre-Yves Strub | 19 November 2015, 10:49:20 UTC | Lossless result on standard distributions. | 19 November 2015, 10:56:06 UTC |
| b3e98cf | Pierre-Yves Strub | 19 November 2015, 10:49:07 UTC | Nits in Int/List. | 19 November 2015, 10:56:05 UTC |
| bf155c7 | Pierre-Yves Strub | 18 November 2015, 20:55:04 UTC | Nits in List && Int. | 18 November 2015, 20:55:04 UTC |
| 697a2a8 | Pierre-Yves Strub | 18 November 2015, 20:11:53 UTC | Kill remaining admits in List. | 18 November 2015, 20:12:02 UTC |
| 985950d | Pierre-Yves Strub | 18 November 2015, 18:36:23 UTC | Nits in List. | 18 November 2015, 18:36:36 UTC |
| 3b99041 | Pierre-Yves Strub | 18 November 2015, 17:09:21 UTC | Proof of perm_allpairs | 18 November 2015, 17:09:21 UTC |
| a0d5e83 | Pierre-Yves Strub | 18 November 2015, 17:08:50 UTC | Allow `apply` / `exact` to act using the top assumption. | 18 November 2015, 17:08:50 UTC |
| 2dbec85 | Pierre-Yves Strub | 18 November 2015, 16:38:57 UTC | Proof refactoring in List. | 18 November 2015, 16:38:57 UTC |
| 9f8c7a1 | Pierre-Yves Strub | 18 November 2015, 15:44:06 UTC | Nits in List. | 18 November 2015, 15:44:36 UTC |
| 491a6f4 | Benjamin Gregoire | 18 November 2015, 14:30:28 UTC | sort the result of search, most relevant clause at the end. | 18 November 2015, 14:42:00 UTC |
| b1c3bba | Benjamin Gregoire | 16 November 2015, 09:47:00 UTC | improve theory Indepi. weaken hypothesis | 18 November 2015, 14:38:30 UTC |
| 7e470e4 | Pierre-Yves Strub | 18 November 2015, 13:29:24 UTC | Admit some properties about allpairs. | 18 November 2015, 13:29:24 UTC |
| b7368cc | Pierre-Yves Strub | 18 November 2015, 12:59:14 UTC | Fix extra args. | 18 November 2015, 12:59:29 UTC |
| 63274eb | Pierre-Yves Strub | 18 November 2015, 12:08:26 UTC | Bits in bigops + big_allpairs. | 18 November 2015, 12:36:39 UTC |
| aa567fe | Pierre-Yves Strub | 18 November 2015, 12:08:16 UTC | Nits on allpairs. | 18 November 2015, 12:36:38 UTC |
| dafd55b | Pierre-Yves Strub | 18 November 2015, 11:46:35 UTC | Tuple: nits + some combinatorial results. | 18 November 2015, 11:46:59 UTC |
| 6799d54 | Pierre-Yves Strub | 18 November 2015, 11:45:03 UTC | List: allpairs def. + spec. (= cross-product \o map) | 18 November 2015, 11:46:56 UTC |
| 4091703 | Pierre-Yves Strub | 18 November 2015, 11:42:59 UTC | Nits in Lists (eq. spec. for cons/cat + hasPn). | 18 November 2015, 11:46:55 UTC |
