source: src/ASM @ 1810

Name Size Rev Age Author Last Change
../
CPP2011 1033   10 years sacerdot ispelled & submitted
Assembly.ma 50.9 KB 1668   9 years boender - split build_maps into build_maps and build_maps_ok - work with CSC …
AssemblyProof.ma 88.2 KB 1668   9 years boender - split build_maps into build_maps and build_maps_ok - work with CSC …
BitVectorTrie.ma 24.2 KB 1632   9 years boender - strengthened insert_lookup_opt
Policy.ma 61.5 KB 1810   9 years boender - new version of policy that compiles up to the final glue
Char.ma 76 bytes 697   10 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
Arithmetic.ma 12.4 KB 1646   9 years mulligan finished the block_costs computation, and propagated the changes …
ASM.ma 9.0 KB 1522   9 years mulligan changes to preamble and lin to asm pass, resolved conflict in interpret
ASMCosts.ma 73.3 KB 1807   9 years mulligan some changes, as finally worked out what i was up to prior to working …
CostsProof.ma 30.9 KB 1695   9 years mulligan Progress on CostsProof?.ma file.
Fetch.ma 23.5 KB 1642   9 years mulligan finished big proof in all but two cases
Interpret.ma 36.5 KB 1710   9 years mulligan changes from friday afternoon
README 641 bytes 431   10 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
StatusProofs.ma 13.2 KB 1710   9 years mulligan changes from friday afternoon
Util.ma 19.5 KB 1602   9 years mulligan giving up on fetch proofs for time being
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
BitVectorZ.ma 4.0 KB 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
Erase.ma 3.5 KB 1600   9 years sacerdot utilities and ASM ported to the new standard library
FoldStuff.ma 1.7 KB 1600   9 years sacerdot utilities and ASM ported to the new standard library
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.
Status.ma 47.0 KB 1666   9 years sacerdot PreStatus? datatype change: the code_memory field is not a left …
String.ma 90 bytes 1599   9 years sacerdot Start of merging of stuff into the standard library of Matita.
BitVector.ma 6.4 KB 1635   9 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
I8051.ma 6.9 KB 1635   9 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
Note: See TracBrowser for help on using the repository browser.