source: src/ASM @ 1879

Name Size Rev Age Author Last Change
../
CPP2011 1033   9 years sacerdot ispelled & submitted
Arithmetic.ma 13.1 KB 1870   9 years boender - changed sigma00 in Assembly to use foldl_strong + proved invariants …
ASM.ma 9.0 KB 1522   9 years mulligan changes to preamble and lin to asm pass, resolved conflict in interpret
ASMCosts.ma 78.6 KB 1869   9 years mulligan a load of axioms closed in ASMCosts file
Assembly.ma 56.6 KB 1870   9 years boender - changed sigma00 in Assembly to use foldl_strong + proved invariants …
AssemblyProof.ma 88.2 KB 1668   9 years boender - split build_maps into build_maps and build_maps_ok - work with CSC …
BitVector.ma 6.4 KB 1635   9 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
BitVectorTrie.ma 24.2 KB 1632   9 years boender - strengthened insert_lookup_opt
BitVectorZ.ma 4.0 KB 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
Char.ma 76 bytes 697   10 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
CostsProof.ma 30.9 KB 1695   9 years mulligan Progress on CostsProof?.ma file.
Erase.ma 3.5 KB 1600   9 years sacerdot utilities and ASM ported to the new standard library
Fetch.ma 23.5 KB 1642   9 years mulligan finished big proof in all but two cases
FoldStuff.ma 1.7 KB 1600   9 years sacerdot utilities and ASM ported to the new standard library
I8051.ma 6.9 KB 1635   9 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
I8051bis.ma 125 bytes 1415   9 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
Interpret2.ma 2.3 KB 1606   9 years sacerdot Porting to last library of Matita.
Interpret.ma 36.5 KB 1710   9 years mulligan changes from friday afternoon
Policy.ma 76.7 KB 1879   9 years boender - Policy compiles until the end, still some (fairly trivial) cases …
README 641 bytes 431   10 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 47.0 KB 1666   9 years sacerdot PreStatus? datatype change: the code_memory field is not a left …
StatusProofs.ma 13.2 KB 1710   9 years mulligan changes from friday afternoon
String.ma 90 bytes 1599   9 years sacerdot Start of merging of stuff into the standard library of Matita.
Util.ma 19.6 KB 1811   9 years boender - corrected definition of geb
Vector.ma 17.8 KB 1646   9 years mulligan finished the block_costs computation, and propagated the changes …
WellLabeled.ma 6.9 KB 1494   9 years mulligan changes to get everything compiling again
Note: See TracBrowser for help on using the repository browser.