Map
lang
MapArray
spec
MapArrayLemmas
spec
MapArrayList
spec
MinLemmas
proof
MinOps
proof
MonadStateLaws
state
map
List
Option
State
List
PList
MapArray
mapList
PList
mapM
State
mapM_
State
mapToFlatMap
MonadStateLaws
max
MinOps
merge
SortedListTakeOps
AHeap
ArrayHeap
DistinctSortedListOps
IntSet
LeftistHeap
LeftistHeapOps
ListHeap
PairMapSpec
mergeSortedList
SortedListOps
merge_assoc
DistinctSortedListSpec
merge_assoc_lemma
SortedListTakeLemmas
DistinctSortedListLemmas
FIFOMapSpec
PairMapSpec
SetMapSpec
merge_assoc_prop
Heap_List_BisimulationSpec
LeftistHeapSpec
LeftistHeapSpec0
merge_associative_prop
SortedListTakeSpec
merge_bisim
ArrayHeapListHeapBisim
merge_comm
DistinctSortedListSpec
merge_comm_lemma
SortedListTakeLemmas
DistinctSortedListLemmas
merge_comm_prop
Heap_List_BisimulationSpec
LeftistHeapSpec
LeftistHeapSpec0
merge_commu_lemma
FIFOMapSpec
PairMapSpec
SetMapSpec
merge_commu_lemma2
PairMapSpec
merge_commutative_prop
SortedListTakeSpec
merge_invariant
LeftistHeapSpec
PairMapSpec
merge_not_contains
DistinctSortedListLemmas
merge_op
AHeap
merge_perm
AHeap
LeftistHeap
merge_perm_lemma
SetMapLemmas
min
MinOps
SetAggregationProof
min_concat_comm
MinLemmas
min_concat_lemma
MinLemmas
min_contains
MinLemmas
min_content
MinLemmas
min_delete
MinLemmas
SortedListTakeLemmas
min_head_lemma
SortedListLemmas
min_lemma
MinLemmas
min_lemma2
MinLemmas
min_not_contains
MinLemmas
min_permutation
MinLemmas
min_sort_lemma
SortedListLemmas
modify
State
monads
leon
monotonic
annotation