source:
src/ASM
@
1487
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| CPP2011 | 1033 | 8 years | ispelled & submitted | ||
| Arithmetic.ma | 12.1 KB | 1485 | 8 years | Less nice definitiion of add_with_carries that avoids a quadratic … | |
| ASM.ma | 8.7 KB | 1112 | 8 years | got lin > asm stuff working | |
| ASMCosts.ma | 9.9 KB | 1486 | 8 years | finished asm costs | |
| Assembly.ma | 66.0 KB | 1482 | 8 years | 1. very long standing conflict committed (but don't ask me what the … | |
| AssemblyProof.ma | 88.7 KB | 1484 | 8 years | … | |
| BitVector.ma | 6.1 KB | 990 | 8 years | Do no longer use the daemon automatically :-) | |
| BitVectorTrie.ma | 23.5 KB | 1479 | 8 years | - added insert_lookup_opt - assembly compiles now | |
| BitVectorZ.ma | 4.0 KB | 891 | 9 years | Revise proofs affected by recent matita change. | |
| Char.ma | 76 bytes | 697 | 9 years | Merge Clight branch of vectors and friends. Start making stuff build. | |
| Erase.ma | 3.5 KB | 1463 | 8 years | added erasure for lin | |
| Fetch.ma | 22.0 KB | 895 | 9 years | Fetch function fixed: alla AJMPS were ACALL (and the other way around) … | |
| FoldStuff.ma | 1.7 KB | 1062 | 8 years | separated jmeq and coercions from foldstuff.ma in order to fix the … | |
| I8051.ma | 7.2 KB | 1416 | 8 years | Maps from hardware registers to beval now implemented in ASM/I8051 (in … | |
| I8051bis.ma | 125 bytes | 1415 | 8 years | 1. hwreg_store/retrieve no longer returns a res (but it is still … | |
| Interpret2.ma | 2.4 KB | 1478 | 8 years | Almost completed (up to is_finals). | |
| Interpret.ma | 30.5 KB | 1037 | 8 years | Main theorem: comments are working again. | |
| JMCoercions.ma | 823 bytes | 1335 | 8 years | Ported to new Matita stdlib. | |
| README | 641 bytes | 431 | 9 years | - README updated - Test and DoTest? fixed to work on assembly_program - … | |
| Status.ma | 45.3 KB | 1459 | 8 years | - moved stronger occurs_exactly_once lemma to its proper place in … | |
| StatusProofs.ma | 9.1 KB | 1014 | 8 years | The main theorem is completely broken (again). | |
| String.ma | 84 bytes | 698 | 9 years | Commit with changes to files to get our files to typecheck. | |
| Util.ma | 22.4 KB | 1323 | 8 years | Reduce number of notations for destructive let on pairs to one. | |
| Vector.ma | 17.7 KB | 1330 | 8 years | Evict obsolete file. | |
| WellLabeled.ma | 1.9 KB | 1487 | 8 years | committing some code for well labelling | |
|
|||||||||||||
Note: See TracBrowser
for help on using the repository browser.
