+ module Data.Crystal
+ import Data.List
+ import Data.Maybe
+
+ e' : Nat -> Nat -> Ordering
+ e' i j =
+ if i == j then GT
+ else if j == S i then LT
+ else EQ
+
+ f' : Nat -> Nat -> Ordering
+ f' i = contra . f' i
+
+ scan : Ordering -> Nat -> Maybe Nat
+ scan LT Z = Nothing
+ scan LT (S x) = Just x
+ scan EQ x = Just x
+ scan GT x = Just $ S $ x
+
+ scanner : (Nat, Nat, Nat) -> Ordering -> (Nat, Nat, Nat)
+ scanner (x, y, z) w with (scan w z)
+ _ | Nothing = (S x, S x, Z)
+ _ | (Just v) = (S x, y, v)
+
+ fi : List Ordering -> Maybe Nat
+ fi x = let (_, p, _) = foldl scanner (0,0,0) x in p
+
+ export
+ e : Nat -> List Nat -> Maybe $ List Nat
+ export
+ f : Nat -> List Nat -> Maybe $ List Nat
+
+ f i x = pure $ replaceAt !(scan LT $ fi $ f' i <$> x) (S i) x @{?idris_baka}