|
../
|
|
CPP2011
|
|
1033
|
2 years
|
sacerdot:
ispelled & submitted
|
|
SEFM2012
|
|
1889
|
13 months
|
boender:
- some pages of article
|
|
Arithmetic.ma
|
13.1 KB |
1870
|
14 months
|
boender:
- changed sigma00 in Assembly to use foldl_strong + proved invariants
- …
|
|
ASM.ma
|
9.0 KB |
1882
|
14 months
|
tranquil:
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
ASMCosts.ma
|
59.9 KB |
1910
|
13 months
|
mulligan:
Finished proof modulo termination argument
|
|
ASMCostsSplit.ma
|
16.9 KB |
1899
|
13 months
|
mulligan:
Changes to statements of theorems
|
|
Assembly.ma
|
56.9 KB |
1905
|
13 months
|
boender:
- plugging gap in assembly proof
|
|
AssemblyProof.ma
|
88.2 KB |
1668
|
16 months
|
boender:
- split build_maps into build_maps and build_maps_ok
- work with CSC on …
|
|
BitVector.ma
|
6.5 KB |
1890
|
13 months
|
boender:
- added comment about bitvector translation
|
|
BitVectorTrie.ma
|
24.2 KB |
1632
|
17 months
|
boender:
- strengthened insert_lookup_opt
|
|
BitVectorZ.ma
|
4.0 KB |
1516
|
18 months
|
sacerdot:
Ported to syntax of Matita 0.99.1.
|
|
Char.ma
|
76 bytes |
697
|
2 years
|
campbell:
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
CostsProof.ma
|
33.6 KB |
1910
|
13 months
|
mulligan:
Finished proof modulo termination argument
|
|
Erase.ma
|
3.5 KB |
1600
|
18 months
|
sacerdot:
utilities and ASM ported to the new standard library
|
|
Fetch.ma
|
23.5 KB |
1642
|
17 months
|
mulligan:
finished big proof in all but two cases
|
|
FoldStuff.ma
|
1.7 KB |
1600
|
18 months
|
sacerdot:
utilities and ASM ported to the new standard library
|
|
I8051.ma
|
6.9 KB |
1635
|
17 months
|
tranquil:
* lists with binders and monads
* Joint.ma and other temprarily forked, …
|
|
I8051bis.ma
|
125 bytes |
1415
|
19 months
|
sacerdot:
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
Interpret2.ma
|
2.3 KB |
1606
|
17 months
|
sacerdot:
Porting to last library of Matita.
|
|
Interpret.ma
|
48.0 KB |
1910
|
13 months
|
mulligan:
Finished proof modulo termination argument
|
|
Policy.ma
|
77.2 KB |
1886
|
14 months
|
boender:
- improvements for disambiguation and quick(er) typing
|
|
README
|
0.6 KB |
431
|
2 years
|
mulligan:
- README updated
- Test and DoTest? fixed to work on assembly_program
- …
|
|
Status.ma
|
40.3 KB |
1882
|
14 months
|
tranquil:
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
StatusProofs.ma
|
13.2 KB |
1710
|
15 months
|
mulligan:
changes from friday afternoon
|
|
String.ma
|
90 bytes |
1599
|
18 months
|
sacerdot:
Start of merging of stuff into the standard library of Matita.
|
|
Util.ma
|
23.3 KB |
1908
|
13 months
|
fguidi:
notation fixup following last commit of matita
we shifted the levels of …
|
|
Vector.ma
|
17.8 KB |
1908
|
13 months
|
fguidi:
notation fixup following last commit of matita
we shifted the levels of …
|
|
WellLabeled.ma
|
6.9 KB |
1494
|
19 months
|
mulligan:
changes to get everything compiling again
|
