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)
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
