source: src/ASM @ 1517

Name Size Rev Age Author Last Change
../
CPP2011 1033   10 years sacerdot ispelled & submitted
ASM.ma 9.0 KB ​ 1515   9 years campbell Add type of maps on positive binary numbers, and use them for …
Char.ma 76 bytes ​ 697   10 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
Erase.ma 3.5 KB ​ 1515   9 years campbell Add type of maps on positive binary numbers, and use them for …
I8051.ma 7.2 KB ​ 1515   9 years campbell Add type of maps on positive binary numbers, and use them for …
Interpret2.ma 2.4 KB ​ 1515   9 years campbell Add type of maps on positive binary numbers, and use them for …
Interpret.ma 30.8 KB ​ 1515   9 years campbell Add type of maps on positive binary numbers, and use them for …
StatusProofs.ma 9.1 KB ​ 1515   9 years campbell Add type of maps on positive binary numbers, and use them for …
ASMCosts.ma 11.1 KB ​ 1497   9 years mulligan a bit of tidying up, removing dead code, etc.
Assembly.ma 66.0 KB ​ 1493   9 years mulligan finished well labeled check, up to injectivity of the label map
CostsProof.ma 29.2 KB ​ 1514   9 years mulligan changes from today. matita keeps dieing
FoldStuff.ma 1.7 KB ​ 1062   10 years mulligan separated jmeq and coercions from foldstuff.ma in order to fix the …
README 641 bytes ​ 431   10 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
String.ma 84 bytes ​ 698   10 years mulligan Commit with changes to files to get our files to typecheck.
WellLabeled.ma 6.9 KB ​ 1494   9 years mulligan changes to get everything compiling again
Arithmetic.ma 12.1 KB ​ 1485   9 years sacerdot Less nice definitiion of add_with_carries that avoids a quadratic …
AssemblyProof.ma 88.7 KB ​ 1484   9 years sacerdot …
BitVector.ma 6.1 KB ​ 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
BitVectorTrie.ma 23.5 KB ​ 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
BitVectorZ.ma 4.0 KB ​ 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
Fetch.ma 22.0 KB ​ 895   10 years sacerdot Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
I8051bis.ma 125 bytes ​ 1415   9 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
JMCoercions.ma 823 bytes ​ 1335   9 years sacerdot Ported to new Matita stdlib.
Status.ma 44.9 KB ​ 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
Util.ma 22.3 KB ​ 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
Vector.ma 17.7 KB ​ 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
Note: See TracBrowser for help on using the repository browser.