source: src/common @ 2105

Name Size Rev Age Author Last Change
../
Animation.ma 4.6 KB 1993   9 years campbell Make front-end memory model only depend on the general definitions by …
AssocList.ma 767 bytes 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
AST.ma 27.0 KB 2105   9 years campbell Show some results about globalenvs and program transformations.
ByteValues.ma 6.1 KB 1987   9 years campbell Move BEValues to common to reflect their use in the memory model for …
CostLabel.ma 233 bytes 1268   10 years sacerdot 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
Errors.ma 8.0 KB 1954   9 years campbell Initial state is in the labelling simulation (modulo global envs results).
Events.ma 10.8 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Floats.ma 2.7 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
FrontEndMem.ma 1.6 KB 1993   9 years campbell Make front-end memory model only depend on the general definitions by …
FrontEndOps.ma 22.4 KB 2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
FrontEndVal.ma 2.8 KB 2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
GenMem.ma 7.1 KB 2105   9 years campbell Show some results about globalenvs and program transformations.
Globalenvs.ma 60.9 KB 2105   9 years campbell Show some results about globalenvs and program transformations.
Graphs.ma 1.6 KB 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
Identifiers.ma 25.3 KB 1949   9 years tranquil * lemma trace rel to eq flatten trace * some more properties of …
Integers.ma 77.6 KB 2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
IO.ma 2.6 KB 961   10 years campbell Use precise bitvector sizes throughout the front end, rather than …
IOMonad.ma 13.6 KB 2044   9 years campbell PCs for RTLabs structured traces.
LabelledObjects.ma 9.8 KB 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
Order.ma 117 bytes 1049   10 years mulligan more stuff added
Pointers.ma 5.0 KB 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
PositiveMap.ma 7.7 KB 2104   9 years campbell Fill in misc axiom.
PreIdentifiers.ma 582 bytes 1515   10 years campbell Add type of maps on positive binary numbers, and use them for …
Registers.ma 436 bytes 1129   10 years mulligan removed conversions between Register and register
Smallstep.ma 27.7 KB 1510   10 years sacerdot All files ported to new dependent inversion.
SmallstepExec.ma 4.7 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
StructuredTraces.ma 27.3 KB 2044   9 years campbell PCs for RTLabs structured traces.
Values.ma 29.9 KB 2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
Note: See TracBrowser for help on using the repository browser.