[Ur] Undocumented folder functionality?

[Adam Chlipala]

Ron de Bruijn wrote:
> 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.

I expect you're looking in top.ur, which _defines_ [folder].  Outside 
that module, the type family is abstract and definitely may not be 
treated as a 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)