rename functions

leesongun

Mar 10, 2023, 11:59 PM

J5S73FCKLNL2LIZW3SWYM7ADQ4K7QQMP24YA6DPLMO2UOYSTBPCQC

Dependencies

• [2] CMHGXE7Y concise implementation (type theoretically and computationally slightly worse)
• [3] VLK55FT2 initial implementation of crystal operators

Change contents

• replacement in Data/Crystal.idr at line 8
  [3.167]→[3.167:205](∅→∅)
  − e' : Nat -> Nat -> Ordering

  − e' i j =
  [3.167]

  [3.205]
  + -- U_q(\mathcal{g}) q->0 limit

  + -- idk about superalgebra case

  + --todo: prove braiding relation

  + --todo: prove that we change i -> i+1

  +

  + paren : Nat -> Nat -> Ordering

  + paren i j =
• replacement in Data/Crystal.idr at line 19
  [3.269]→[3.269:319](∅→∅),[3.319]→[2.33:158](∅→∅)
  − f' : Nat -> Nat -> Ordering

  − f' i = contra . e' 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
  [3.269]

  [3.484]
  + (+) : Ordering -> Nat -> Maybe Nat

  + LT + Z = Nothing

  + LT + (S x) = Just x

  + EQ + x = Just $ x

  + GT + x = Just $ S $ x
• replacement in Data/Crystal.idr at line 25
  [3.485]→[2.159:273](∅→∅)
  − scanner : (Maybe $ Fin n, Nat) -> (Ordering, Fin n) -> (Maybe $ Fin n, Nat)

  − scanner (x, y) (w, z) with (scan w y)
  [3.485]

  [2.273]
  + scan : (Maybe $ Fin n, Nat) -> (Ordering, Fin n) -> (Maybe $ Fin n, Nat)

  + scan (x, y) (w, z) with (w + y)
• replacement in Data/Crystal.idr at line 30
  [3.655]→[2.330:441](∅→∅)
  − fi : {n : Nat} -> Vect n Ordering -> Maybe $ Fin n

  − fi a = fst $ foldl scanner (Nothing, Z) $ zip a $ allFins n
  [3.655]

  [3.697]
  + argmin : {n : Nat} -> Vect n Ordering -> Maybe $ Fin n

  + argmin a = fst $ foldl scan (Nothing, Z) $ zip a $ allFins n
• replacement in Data/Crystal.idr at line 35
  [3.907]→[2.457:526](∅→∅)
  − e i x = pure $ replaceAt (complement !(fi $ e' i <$> reverse x)) i x
  [3.907]

  [3.982]
  + e i x = pure $ replaceAt (complement !(argmin $ paren i <$> reverse x)) i x
• replacement in Data/Crystal.idr at line 39
  [2.598]→[2.598:650](∅→∅)
  − f i x = pure $ replaceAt !(fi $ f' i <$> x) (S i) x
  [2.598]
  + f i x = pure $ replaceAt !(argmin $ (contra . paren i) <$> x) (S i) x