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