|
../
|
|
CPP2011
|
|
1033
|
10 years
|
sacerdot |
ispelled & submitted
|
|
SEFM2012
|
|
1889
|
9 years
|
boender |
- some pages of article
|
|
AbstractStatus.ma
|
2.0 KB
|
1944
|
9 years
|
sacerdot |
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
|
|
Arithmetic.ma
|
17.7 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
ASM.ma
|
9.0 KB
|
1882
|
9 years
|
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
ASMCosts.ma
|
35.4 KB
|
1938
|
9 years
|
sacerdot |
Definitions moved to the right places, now everything compiles again.
|
|
ASMCostsSplit.ma
|
11.6 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
Assembly.ma
|
57.2 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
AssemblyProof.ma
|
89.7 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
BitVector.ma
|
6.7 KB
|
1928
|
9 years
|
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
BitVectorTrie.ma
|
24.3 KB
|
1931
|
9 years
|
boender |
- added latest bvt alias
- temporary "cases daemon" commit of new …
|
|
BitVectorZ.ma
|
4.0 KB
|
1516
|
9 years
|
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
Char.ma
|
76 bytes
|
697
|
10 years
|
campbell |
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
CostsProof.ma
|
32.5 KB
|
1935
|
9 years
|
mulligan |
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
|
|
Erase.ma
|
3.5 KB
|
1600
|
9 years
|
sacerdot |
utilities and ASM ported to the new standard library
|
|
Fetch.ma
|
23.5 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
FoldStuff.ma
|
1.7 KB
|
1600
|
9 years
|
sacerdot |
utilities and ASM ported to the new standard library
|
|
I8051.ma
|
6.9 KB
|
1635
|
9 years
|
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
I8051bis.ma
|
125 bytes
|
1415
|
9 years
|
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
Interpret2.ma
|
2.3 KB
|
1606
|
9 years
|
sacerdot |
Porting to last library of Matita.
|
|
Interpret.ma
|
47.1 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
Policy.ma
|
72.8 KB
|
1942
|
9 years
|
mulligan |
Work on showing the equivalence of two methods of looking up from the maps.
|
|
README
|
641 bytes
|
431
|
10 years
|
mulligan |
- README updated
- Test and DoTest? fixed to work on assembly_program
- …
|
|
Status.ma
|
40.3 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
StatusProofs.ma
|
13.2 KB
|
1710
|
9 years
|
mulligan |
changes from friday afternoon
|
|
String.ma
|
90 bytes
|
1599
|
9 years
|
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
Util.ma
|
32.8 KB
|
1937
|
9 years
|
boender |
- filled in some of the gaps in the proof of Policy
- reverted …
|
|
UtilBranch.ma
|
2.2 KB
|
1946
|
9 years
|
sacerdot |
\snd half_add => add everywhere
|
|
Vector.ma
|
17.8 KB
|
1908
|
9 years
|
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
WellLabeled.ma
|
6.9 KB
|
1494
|
9 years
|
mulligan |
changes to get everything compiling again
|
