http://impredicative.com/ur/tutorial/tlc.html shows this example:
type nat = t :: Type -> t -> (t -> t) -> t val zero : nat = fn [t :: Type] (z : t) (s : t -> t) => z fun succ (n : nat) : nat = fn [t :: Type] (z : t) (s : t -> t) => s (n [t] z s) val one = succ zero val two = succ one val three = succ two three [int] 0 (plus 1) == 3 three [string] "" (strcat "!") == "!!!" Eg the succ function has t in its return type and in it n:nat arg. So should urweb be able to deduce type of t automatically? Should it be possible to replace the explicit :: by an implicit t ::: Type ? Trying to do so I get some unification errors - is it because I removed some [t] like args incorrectly? Marc Weber _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
