implement dependent fold

leesongun

Mar 10, 2023, 9:44 PM

65A27CAQULABDHBVYQPTB6LUM6UZ4S3UTJ4Z753KSZTFPXVHTMBQC

Dependencies

• [2] VCJVFB63 add total ordering

Change contents

• file addition: Fold.idr (----------)
  [2.19]
  + module Control.Fold

  +

  + import Data.Vect

  +

  + dfoldl : {b : Nat -> Type} -> ((m : Nat) -> b m -> a -> b (S m)) -> b Z -> Vect n a -> b n

  + dfoldl f z [] = z

  + 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