Open chshersh opened 5 years ago
This is a meta-issue to collect all possible laws for the Treap data structure:
Treap
measure (one x) ≡ x
IsList
toList . fromList ≡ id
at i . insert i x ≡ Just x
delete i . insert i x ≡ id
size (insert i x t) ≡ size t + 1
uncurry merge . splitAt i ≡ id
size (merge l r) ≡ size l + size r
measure (merge l r) ≡ measure l <> measure r
splitAt i t ≡ (take i t, drop i t)
This is a meta-issue to collect all possible laws for the
Treap
data structure:Semigroup/Monoid laws
Measured
measure (one x) ≡ x
IsList
IsList
:toList . fromList ≡ id
Modifications
at i . insert i x ≡ Just x
delete i . insert i x ≡ id
size (insert i x t) ≡ size t + 1
Cuts
uncurry merge . splitAt i ≡ id
size (merge l r) ≡ size l + size r
measure (merge l r) ≡ measure l <> measure r
splitAt i t ≡ (take i t, drop i t)