SPlactic.idr
module Data.SPlactic
infixl 7 <<
(<<) : SnocList Nat -> Nat -> SnocList Nat
xs :< x :< y << z =
if x <= y && x > z
then xs :< x << z :< y
else if x <= z && y > z
then xs :< y << x :< z
else xs :< x :< y :< z
xs << x = xs :< x
norm : SnocList Nat -> SnocList Nat
norm [<] = [<]
norm $ xs :< x = norm xs << x