

@465

9 years 
mulligan 
Moved over to standard library.



@462

9 years 
mulligan 
Added bitvector arithmetic for Brian.



@410

9 years 
mulligan 
Using bitvectortries for a dictionary doesn't work even if we …



@374

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



@362

9 years 
sacerdot 
Less ambiguous definitions.



@357

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



@353

9 years 
mulligan 
 pc was initialized to 7 in place of sp
 bitvector_of_nat was …



@351

9 years 
mulligan 
No more axioms but the paralogisms.



@349

9 years 
mulligan 
Added fold_right_i (with dependent type) to List file.



@343

9 years 
mulligan 
Fixed Status.ma so that it compiles.



@337

9 years 
mulligan 
Changes to execute_1 file. Changes to get everything type checking.



@330

9 years 
mulligan 
Fixed segmentation fault in Nat.ma, added get_index and renamed …



@320

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



@315

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



@314

9 years 
mulligan 
Finished all get_ and set_arg_* functions.



@313

9 years 
mulligan 
Added axioms for addition for claudio.



@275

9 years 
mulligan 
Removed all axioms from Arithmetic.ma and replaced them with …



@273

9 years 
mulligan 
Some fault functions were rewritten.



@271

9 years 
sacerdot 
assembly1 defined on ACALL and ADD: it seems it will become too slow…



@270

9 years 
mulligan 
More added.



@269

9 years 
sacerdot 
 …



@266

9 years 
mulligan 
Changes to bitvector.



@263

9 years 
sacerdot 
 use standard notation for exponential
 Bit is now Bool



@262

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



@260

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



@257

9 years 
mulligan 
Added exponential functions for nats. Working on operational …



@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 …



@240

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



@238

9 years 
mulligan 
More work on bitvectors.



@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.



@235

9 years 
mulligan 
More work on bitvectors.



@234

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



@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.



@228

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


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



@224

9 years 
mulligan 
Changes to bit vectors and vectors.
