add test implementation of Plactic monoid

leesongun

Mar 9, 2023, 11:13 PM

ZAH4MBPK5B5DHU5PCSCLDF2RLF3SBPJCZ7VUHT6M73NT6TFWNAIAC

Dependencies

• [2] ROKTK7EK add SUSY degree

Change contents

• file addition: SPlactic.idr (----------)
  [2.16]
  + 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