source: src/utilities @ 2244

Name Size Rev Age Author Last Change
../
binary 1628   9 years campbell Show that the universe generated by Clight/fresh.ma is good.
adt 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
trace.ma 895 bytes 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
state.ma 1.4 KB 1976   9 years tranquil * monads: just changed some defs, which had to be propagated in some …
setoids.ma 1.4 KB 1635   9 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
RegisterSet.ma 1.7 KB 1193   10 years mulligan work on colouring algorithm halted as it can be axiomatised. now …
proper.ma 756 bytes 1908   9 years fguidi notation fixup following last commit of matita we shifted the levels …
permutations.ma 10.5 KB 1976   9 years tranquil * monads: just changed some defs, which had to be propagated in some …
option.ma 2.6 KB 1976   9 years tranquil * monads: just changed some defs, which had to be propagated in some …
monad.ma 11.9 KB 2179   9 years campbell Dependent pair monad binding notation.
lists.ma 8.6 KB 1949   9 years tranquil * lemma trace rel to eq flatten trace * some more properties of …
hide.ma 1.2 KB 2200   9 years tranquil * updated joint semantics: generation of linear and graph semantics * …
fixpoints.ma 785 bytes 2174   9 years tranquil * factored out script for (axiomatised) fixpoint computation * ERTL → …
extranat.ma 3.4 KB 1593   10 years boender - cleaned up Assembly, moved some definitions elsewhere
extralib.ma 6.9 KB 2178   9 years campbell Shift some notation into utilities.
Coqlib.ma 31.7 KB 1600   10 years sacerdot utilities and ASM ported to the new standard library
BitVectorTrieSet.ma 2.2 KB 753   10 years mulligan Work from today.
bindLists.ma 1.3 KB 2155   9 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
bind_new.ma 3.3 KB 1976   9 years tranquil * monads: just changed some defs, which had to be propagated in some …
Note: See TracBrowser for help on using the repository browser.