source: src/common @ 2300

Name Size Rev Age Author Last Change
../
Values.ma 29.8 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
StructuredTraces.ma 33.5 KB 2299   9 years campbell Soundly labelled RTLabs structured traces are "unrepeating".
SmallstepExec.ma 6.2 KB 2203   9 years campbell A general result about simulations of executions.
Smallstep.ma 27.7 KB 1510   10 years sacerdot All files ported to new dependent inversion.
Registers.ma 444 bytes 2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
PreIdentifiers.ma 582 bytes 1515   10 years campbell Add type of maps on positive binary numbers, and use them for …
PositiveMap.ma 7.7 KB 2104   9 years campbell Fill in misc axiom.
Pointers.ma 5.9 KB 2296   9 years campbell Tidy up some ill-placed definitions.
Order.ma 117 bytes 1049   10 years mulligan more stuff added
LabelledObjects.ma 10.3 KB 2133   9 years boender - moved does_not_occur_occur_absurd
IOMonad.ma 14.3 KB 2145   9 years campbell Cost labelling doesn't affect interaction.
IO.ma 2.6 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
Integers.ma 77.6 KB 2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
Identifiers.ma 26.4 KB 2222   9 years sacerdot More robust to possible future changes to the "in match" semantics …
Graphs.ma 1.6 KB 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
Globalenvs.ma 64.0 KB 2226   9 years campbell Whole program proof.
GenMem.ma 7.2 KB 2185   9 years campbell Use bitvectors for offsets.
FrontEndVal.ma 2.9 KB 2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
FrontEndOps.ma 22.3 KB 2177   9 years campbell Tidy up multiplication.
FrontEndMem.ma 1.6 KB 2185   9 years campbell Use bitvectors for offsets.
Floats.ma 2.7 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Executions.ma 7.0 KB 2206   9 years campbell Add note about cost maps to simulation definition.
Events.ma 10.8 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Errors.ma 8.0 KB 1954   9 years campbell Initial state is in the labelling simulation (modulo global envs results).
CostLabel.ma 233 bytes 1268   10 years sacerdot 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
ByteValues.ma 8.4 KB 2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
BackEndOps.ma 7.1 KB 2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
AST.ma 27.6 KB 2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
AssocList.ma 767 bytes 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Animation.ma 4.6 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
Note: See TracBrowser for help on using the repository browser.