source: src/ASM @ 1461

Name Size Rev Age Author Last Change
../
CPP2011 1033   8 years sacerdot ispelled & submitted
Arithmetic.ma 11.8 KB 1426   8 years boender removed axiom
ASM.ma 8.7 KB 1112   8 years mulligan got lin > asm stuff working
Assembly.ma 63.7 KB 1459   8 years boender - moved stronger occurs_exactly_once lemma to its proper place in …
AssemblyProof.ma 88.7 KB 1333   8 years sacerdot Avoid using the name of the construction of jmeq.
BitVector.ma 6.1 KB 990   8 years sacerdot Do no longer use the daemon automatically :-)
BitVectorTrie.ma 22.5 KB 1424   8 years sacerdot 1. fold function over BitVectorTries? moved from ERTLToLTL to …
BitVectorZ.ma 4.0 KB 891   9 years campbell Revise proofs affected by recent matita change.
Char.ma 76 bytes 697   9 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
Erase.ma 3.3 KB 1461   8 years mulligan rewrote erasure for assembly programs
Fetch.ma 22.0 KB 895   9 years sacerdot Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
FoldStuff.ma 1.7 KB 1062   8 years mulligan separated jmeq and coercions from foldstuff.ma in order to fix the …
I8051.ma 7.2 KB 1416   8 years sacerdot Maps from hardware registers to beval now implemented in ASM/I8051 (in …
I8051bis.ma 125 bytes 1415   8 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
Interpret.ma 30.5 KB 1037   8 years sacerdot Main theorem: comments are working again.
JMCoercions.ma 823 bytes 1335   8 years sacerdot Ported to new Matita stdlib.
README 641 bytes 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 45.3 KB 1459   8 years boender - moved stronger occurs_exactly_once lemma to its proper place in …
StatusProofs.ma 9.1 KB 1014   8 years sacerdot The main theorem is completely broken (again).
String.ma 84 bytes 698   9 years mulligan Commit with changes to files to get our files to typecheck.
Util.ma 22.4 KB 1323   8 years campbell Reduce number of notations for destructive let on pairs to one.
Vector.ma 17.7 KB 1330   8 years campbell Evict obsolete file.
Note: See TracBrowser for help on using the repository browser.