# # ChangeLog for Deliverables/D4.1/Matita/BitVector.ma # # Generated by Trac 1.2 # Jan 18, 2021, 6:38:46 AM Wed, 01 Dec 2010 22:27:04 GMT sacerdot [357] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/BitVectorTrie.ma (modified) * Deliverables/D4.1/Matita/Compare.ma (deleted) * Deliverables/D4.1/Matita/DoTest.ma (modified) * Deliverables/D4.1/Matita/Either.ma (modified) * Deliverables/D4.1/Matita/Exponential.ma (modified) * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Maybe.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) * Deliverables/D4.1/Matita/Test.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) * Deliverables/D4.1/Matita/depends (modified) - stupid bug fixed in BitVectorTrie - dependencies minimized, dead ... Wed, 01 Dec 2010 17:40:15 GMT mulligan [353] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) - pc was initialized to 7 in place of sp - bitvector_of_nat was ... Wed, 01 Dec 2010 15:30:46 GMT mulligan [351] * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Exponential.ma (modified) * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) No more axioms but the paralogisms. Wed, 01 Dec 2010 10:18:05 GMT mulligan [349] * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) Added fold_right_i (with dependent type) to List file. Tue, 30 Nov 2010 15:56:42 GMT mulligan [343] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) Fixed Status.ma so that it compiles. Tue, 30 Nov 2010 11:26:45 GMT mulligan [337] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) Changes to execute_1 file. Changes to get everything type checking. Mon, 29 Nov 2010 13:08:52 GMT mulligan [330] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) Fixed segmentation fault in Nat.ma, added get_index and renamed ... Fri, 26 Nov 2010 17:13:26 GMT mulligan [320] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Added fold_right_i, equivalent of O'Caml's fold_right2. Fri, 26 Nov 2010 16:32:34 GMT mulligan [315] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Decidable equality on vectors and its specialisation to bitvectors. Fri, 26 Nov 2010 15:53:56 GMT mulligan [314] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) Finished all get_ and set_arg_* functions. Fri, 26 Nov 2010 14:33:32 GMT mulligan [313] * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) Added axioms for addition for claudio. Wed, 24 Nov 2010 14:40:37 GMT mulligan [275] * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) Removed all axioms from Arithmetic.ma and replaced them with ... Wed, 24 Nov 2010 13:28:34 GMT mulligan [273] * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) Some fault functions were rewritten. Wed, 24 Nov 2010 00:00:41 GMT sacerdot [271] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/Assembly.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/depends (modified) assembly1 defined on ACALL and ADD: it seems it will become too slow... Tue, 23 Nov 2010 17:12:10 GMT mulligan [270] * Deliverables/D4.1/Matita/BitVector.ma (modified) More added. Tue, 23 Nov 2010 17:11:49 GMT sacerdot [269] * Deliverables/D4.1/Matita/Assembly.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) - ... Tue, 23 Nov 2010 16:10:40 GMT mulligan [266] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Changes to bitvector. Tue, 23 Nov 2010 15:43:34 GMT sacerdot [263] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Exponential.ma (modified) - use standard notation for exponential - Bit is now Bool Tue, 23 Nov 2010 15:39:31 GMT sacerdot [262] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) - new notation [[...]] for vectors to reduce ambiguity - ... Tue, 23 Nov 2010 13:30:10 GMT sacerdot [260] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/BitVectorTrie.ma (modified) * Deliverables/D4.1/Matita/Bool.ma (modified) * Deliverables/D4.1/Matita/Connectives.ma (modified) * Deliverables/D4.1/Matita/Either.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Maybe.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Plogic (added) * Deliverables/D4.1/Matita/Plogic/equality.ma (added) * Deliverables/D4.1/Matita/README (added) * Deliverables/D4.1/Matita/Vector.ma (modified) * Deliverables/D4.1/Matita/depends (added) * Deliverables/D4.1/Matita/root (added) - Minimal changes to make it compile with the standard distribution ... Tue, 23 Nov 2010 10:43:14 GMT mulligan [257] * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Exponential.ma (added) * Deliverables/D4.1/Matita/Interpret.ma (added) Added exponential functions for nats. Working on operational ... Mon, 22 Nov 2010 10:43:04 GMT mulligan [248] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/BitVectorTrie.ma (modified) * Deliverables/D4.1/Matita/Compare.ma (added) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) More changes. Added datatype for addressing modes. Mon, 22 Nov 2010 09:05:05 GMT mulligan [246] * Deliverables/D4.1/Matita/Arithmetic.ma (added) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/BitVectorTrie.ma (added) * Deliverables/D4.1/Matita/Bool.ma (modified) * Deliverables/D4.1/Matita/Cartesian.ma (modified) * Deliverables/D4.1/Matita/Equality.ma (added) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Universes.ma (added) * Deliverables/D4.1/Matita/Util.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Added physical file (Arithmetic) for arithmetic on bit vectors, and ... Mon, 15 Nov 2010 09:22:41 GMT mulligan [240] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Updated Vector / BitVector files taken from my Matita library. Fri, 12 Nov 2010 16:09:39 GMT mulligan [238] * Deliverables/D4.1/Matita/BitVector.ma (modified) More work on bitvectors. Fri, 12 Nov 2010 15:51:45 GMT mulligan [237] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) More functions on bitvectors written. Fri, 12 Nov 2010 15:01:48 GMT mulligan [236] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Cartesian.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Strange problem with matita and the Maybe file? Cannot find Maybe.ng. Fri, 12 Nov 2010 13:43:02 GMT mulligan [235] * Deliverables/D4.1/Matita/BitVector.ma (modified) More work on bitvectors. Fri, 12 Nov 2010 13:27:56 GMT mulligan [234] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Division and modulus implemented. All necessary orders on naturals ... Thu, 11 Nov 2010 15:56:59 GMT mulligan [232] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Bool.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Lots of work from today. Writing bitvector library is harder than it ... Thu, 11 Nov 2010 11:27:04 GMT mulligan [231] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) BitVector stuff from this morning: need further development of Nat ... Wed, 10 Nov 2010 16:26:08 GMT mulligan [230] * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Lots of work from today. Tue, 09 Nov 2010 14:27:30 GMT mulligan [228] * Deliverables/D4.1/Matita/BitVector.ma (moved) * Deliverables/D4.1/Matita/Bool.ma (added) * Deliverables/D4.1/Matita/Cartesian.ma (added) * Deliverables/D4.1/Matita/Either.ma (added) * Deliverables/D4.1/Matita/List.ma (added) * Deliverables/D4.1/Matita/Maybe.ma (added) * Deliverables/D4.1/Matita/Nat.ma (added) * Deliverables/D4.1/Matita/Vector.ma (moved) Conjunction, disjunction and 'xorjunction' implemented on bitvectors. ... Mon, 08 Nov 2010 16:04:27 GMT mulligan [224] * Deliverables/D4.1/Matita/BitVectors.ma (modified) * Deliverables/D4.1/Matita/Vectors.ma (modified) Changes to bit vectors and vectors.