module Data.SPlactic
import Data.SnocList
infixl 7 <<
(<<) : SnocList Nat -> Nat -> SnocList Nat
xs :< x :< y << z = 
    if x <= y && x > z
    then xs :< x << z :< y
    else if z >= x && z < y 
    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