source: src/ASM @ 1591

Name Size Rev Age Author Last Change
../
CPP2011 1033   9 years sacerdot ispelled & submitted
Char.ma 76 bytes 697   9 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
String.ma 84 bytes 698   9 years mulligan Commit with changes to files to get our files to typecheck.
I8051bis.ma 125 bytes 1415   8 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
README 641 bytes 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
JMCoercions.ma 823 bytes 1335   8 years sacerdot Ported to new Matita stdlib.
FoldStuff.ma 1.7 KB 1062   9 years mulligan separated jmeq and coercions from foldstuff.ma in order to fix the …
Interpret2.ma 2.4 KB 1550   8 years sacerdot Repaired after use of Russell for execute_1.
Erase.ma 3.5 KB 1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
BitVectorZ.ma 4.0 KB 1516   8 years sacerdot Ported to syntax of Matita 0.99.1.
BitVector.ma 6.1 KB 1521   8 years sacerdot Syntax change in Matita: change what where => change where what.
WellLabeled.ma 6.9 KB 1494   8 years mulligan changes to get everything compiling again
I8051.ma 7.2 KB 1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
ASMCosts.ma 8.1 KB 1591   8 years mulligan work from today
ASM.ma 9.0 KB 1522   8 years mulligan changes to preamble and lin to asm pass, resolved conflict in interpret
StatusProofs.ma 9.2 KB 1530   8 years campbell Update due to Russell changes.
Arithmetic.ma 12.1 KB 1485   8 years sacerdot Less nice definitiion of add_with_carries that avoids a quadratic …
Vector.ma 17.7 KB 1524   8 years boender - adapted files to new Matita syntax
Util.ma 22.3 KB 1516   8 years sacerdot Ported to syntax of Matita 0.99.1.
Fetch.ma 23.5 KB 1591   8 years mulligan work from today
BitVectorTrie.ma 24.0 KB 1553   8 years boender - added lookup_opt_lookup lemma
CostsProof.ma 30.2 KB 1587   8 years mulligan changes from today, including removing indexing of problematic …
Interpret.ma 34.4 KB 1588   8 years sacerdot All goals generated by Russell for execute_1* are now closed, mostly …
Status.ma 46.1 KB 1588   8 years sacerdot All goals generated by Russell for execute_1* are now closed, mostly …
AssemblyProof.ma 88.7 KB 1484   8 years sacerdot
Assembly.ma 90.7 KB 1578   8 years boender - proof of termination of policy completed (needs some clean-up work …
Note: See TracBrowser for help on using the repository browser.