source: src/common @ 2248

Name Size Rev Age Author Last Change
../
StructuredTraces.ma 32.1 KB 2186   9 years tranquil updated joint semantics
Graphs.ma 1.6 KB 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
Smallstep.ma 27.7 KB 1510   9 years sacerdot All files ported to new dependent inversion.
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 …
Floats.ma 2.7 KB 1599   9 years sacerdot Start of merging of stuff into the standard library of Matita.
Events.ma 10.8 KB 1599   9 years sacerdot Start of merging of stuff into the standard library of Matita.
CostLabel.ma 233 bytes 1268   10 years sacerdot 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
AssocList.ma 767 bytes 1599   9 years sacerdot Start of merging of stuff into the standard library of Matita.
Registers.ma 436 bytes 1129   10 years mulligan removed conversions between Register and register
Order.ma 117 bytes 1049   10 years mulligan more stuff added
Values.ma 29.8 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
SmallstepExec.ma 6.2 KB 2203   9 years campbell A general result about simulations of executions.
PreIdentifiers.ma 582 bytes 1515   9 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.7 KB 2218   9 years campbell Separate out cost properties required of RTLabs programs from the …
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 …
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.8 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
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.
Executions.ma 7.0 KB 2206   9 years campbell Add note about cost maps to simulation definition.
Errors.ma 8.0 KB 1954   9 years campbell Initial state is in the labelling simulation (modulo global envs results).
ByteValues.ma 6.2 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
AST.ma 27.6 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
Animation.ma 4.6 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
LabelledObjects.ma 10.3 KB 2133   9 years boender - moved does_not_occur_occur_absurd
Note: See TracBrowser for help on using the repository browser.