# # ChangeLog for Deliverables/D4.1/Matita # # Generated by Trac 1.2 # Jan 18, 2021, 6:21:46 AM Tue, 23 Nov 2010 16:42:20 GMT mulligan [267] * Deliverables/D4.1/Matita/Status.ma (moved) Renamed Interpret to Status. 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 16:05:46 GMT mulligan [265] * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Test commit. Tue, 23 Nov 2010 16:05:07 GMT sacerdot [264] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/Assembly.ma (added) * Deliverables/D4.1/Matita/Char.ma (modified) * Deliverables/D4.1/Matita/String.ma (modified) * Deliverables/D4.1/Matita/depends (modified) - new axiomatic data type for Strings - new file for Assembly 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 14:50:28 GMT mulligan [261] * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) * Deliverables/D4.1/Matita/depends (modified) Strengthened typings of get_ and set_index in Vector file. 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 11:56:26 GMT mulligan [259] * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Need stronger set_ and get_index functions on vectors (current ones ... Tue, 23 Nov 2010 10:43:32 GMT mulligan [258] * Deliverables/D4.1/Matita/Connectives.ma (added) * Deliverables/D4.1/Matita/Interpret.ma (modified) Forgotten files. 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 18:25:53 GMT mulligan [256] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Work on ASM.ma file. Mon, 22 Nov 2010 12:55:07 GMT mulligan [249] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/Char.ma (added) * Deliverables/D4.1/Matita/String.ma (added) More work on defining fundamental datatypes. 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 10:12:56 GMT mulligan [247] * Deliverables/D4.1/Matita/ASM.ma (added) * 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) Changes to get directory to compile. 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:42:20 GMT mulligan [244] * Deliverables/D4.1/Matita/Vector.ma (modified) Vector.ma now compiles. Mon, 15 Nov 2010 09:41:29 GMT mulligan [243] * Deliverables/D4.1/Matita/Util.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Updated Util.ma too. Mon, 15 Nov 2010 09:28:26 GMT mulligan [242] * Deliverables/D4.1/Matita/List.ma (modified) Got List to compile. Mon, 15 Nov 2010 09:26:20 GMT mulligan [241] * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Also needed an updated List.ma. 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 ... Fri, 12 Nov 2010 10:51:18 GMT mulligan [233] * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Nat.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) Changes from this morning: Bool / Prop division = nightmare. 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 16:00:50 GMT mulligan [229] * Deliverables/D4.1/Matita/List.ma (modified) * Deliverables/D4.1/Matita/Util.ma (added) * Deliverables/D4.1/Matita/Vector.ma (modified) More changes. 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. Mon, 08 Nov 2010 13:24:56 GMT mulligan [223] * Deliverables/D4.1/Matita/BitVectors.ma (added) * Deliverables/D4.1/Matita/Vectors.ma (modified) File for bitvector specific stuff added. Mon, 08 Nov 2010 12:53:17 GMT mulligan [222] * Deliverables/D4.1/Matita/Vectors.ma (moved) Datatype for fixed length lists (vectors) as well as some recursive ... Mon, 08 Nov 2010 10:17:39 GMT mulligan [221] * Deliverables/D4.1/Matita (added) * Deliverables/D4.1/Matita/BitVectors.ma (added) Starting formalisation in Matita