

@465

9 years 
mulligan 
Moved over to standard library.



@374

9 years 
sacerdot 
1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons …



@373

9 years 
sacerdot 
Order of declaration of notations changed to put more precise …



@370

9 years 
mulligan 
Most of critical lemma done. Hole remaining that I can't coax matita …



@368

9 years 
mulligan 
All 450 proof obligations closed.



@364

9 years 
mulligan 
Added subvector_with function.



@363

9 years 
mulligan 
Resolved conflicts. Added new get_index' which hides the proof …



@362

9 years 
sacerdot 
Less ambiguous definitions.



@357

9 years 
sacerdot 
 stupid bug fixed in BitVectorTrie?
 dependencies minimized, dead …



@352

9 years 
mulligan 
Do not use ndestruct for injectivity since it introduces StreickerK …



@350

9 years 
mulligan 
less axioms



@340

9 years 
sacerdot 
::: is now used in place of :: for vectors to reduce ambiguity



@329

9 years 
mulligan 
Commit to restore deleted file.



@328

9 years 
mulligan 
Got fold_right_i to type check. Moved eq_rect_Type0 into …



@322

9 years 
sacerdot 
More work on fetch.



@320

9 years 
mulligan 
Added fold_right_i, equivalent of O'Caml's fold_right2.



@316

9 years 
sacerdot 
REGISTER now takes a BitVector? 3



@315

9 years 
mulligan 
Decidable equality on vectors and its specialisation to bitvectors.



@311

9 years 
mulligan 
get_arg_16 complete.



@272

9 years 
mulligan 
Changes from this morning.



@269

9 years 
sacerdot 
 …



@268

9 years 
sacerdot 
 notation moved to proper places
 new function split on Vectors



@266

9 years 
mulligan 
Changes to bitvector.



@265

9 years 
mulligan 
Test commit.



@262

9 years 
sacerdot 
 new notation ...? for vectors to reduce ambiguity
 …



@261

9 years 
mulligan 
Strengthened typings of get_ and set_index in Vector file.



@260

9 years 
sacerdot 
 Minimal changes to make it compile with the standard distribution of …



@259

9 years 
mulligan 
Need stronger set_ and get_index functions on vectors (current ones …



@256

9 years 
mulligan 
Work on ASM.ma file.



@248

9 years 
mulligan 
More changes. Added datatype for addressing modes.



@246

9 years 
mulligan 
Added physical file (Arithmetic) for arithmetic on bit vectors, and …



@244

9 years 
mulligan 
Vector.ma now compiles.



@243

9 years 
mulligan 
Updated Util.ma too.



@241

9 years 
mulligan 
Also needed an updated List.ma.



@240

9 years 
mulligan 
Updated Vector / BitVector? files taken from my Matita library.



@237

9 years 
mulligan 
More functions on bitvectors written.



@236

9 years 
mulligan 
Strange problem with matita and the Maybe file? Cannot find Maybe.ng.



@234

9 years 
mulligan 
Division and modulus implemented. All necessary orders on naturals …



@233

9 years 
mulligan 
Changes from this morning: Bool / Prop division = nightmare.



@232

9 years 
mulligan 
Lots of work from today. Writing bitvector library is harder than it …



@231

9 years 
mulligan 
BitVector? stuff from this morning: need further development of Nat …



@230

9 years 
mulligan 
Lots of work from today.



@229

9 years 
mulligan 
More changes.



@228

9 years 
mulligan 
Conjunction, disjunction and 'xorjunction' implemented on bitvectors. …


copied from Deliverables/D4.1/Matita/Vectors.ma:



@224

9 years 
mulligan 
Changes to bit vectors and vectors.
