update dependent fold

leesongun

Mar 10, 2023, 10:02 PM

NTSW5EF6MXRMQ3W5NRFFSSFJRXLNAFL4DLCWDQS5FSGP5FJMEO4AC

Dependencies

• [2] 65A27CAQ implement dependent fold

Change contents

• edit in Control/Fold.idr at line 4
  [2.72]

  [2.72]
  + import Data.Nat
• replacement in Control/Fold.idr at line 6
  [2.73]→[2.73:164](∅→∅)
  − dfoldl : {b : Nat -> Type} -> ((m : Nat) -> b m -> a -> b (S m)) -> b Z -> Vect n a -> b n
  [2.73]

  [2.164]
  + dfoldl : {b : Nat -> Type} -> ((0 m : Nat) -> b m -> a -> b (S m)) -> b m -> Vect n a -> b (n + m)
• replacement in Control/Fold.idr at line 8
  [2.182]→[2.182:301](∅→∅)
  − dfoldl f z (x::xs) = dfoldl f' (f 0 z x) xs where

  − f' : (m : Nat) -> b (S m) -> a -> b $ S $ S m

  − f' m = f $ S m
  [2.182]
  + dfoldl {n=S n} f z (x::xs) = rewrite plusSuccRightSucc n m in dfoldl f (f m z x) xs