[Ur] Undocumented folder functionality?

[Ron de Bruijn]

Hi,

For a folder it is documented that one can use a value of type [folder 
<something>] as an argument to the fold function, but I don't think the below is 
documented to be possible in the manual. In particular that (fl: folder r) 
apparently is some kind of function.

fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
                       tf -> tr rest -> tr ([nm] ++ rest))
            (i : tr []) [r ::: {Unit}] (fl : folder r) =
     fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
        (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
            f [nm] [rest] r.nm (acc (r -- nm)))
        (fn _ => i)

-- 
Best regards,
   Ron de Bruijn