Mercurial > urweb

comparison lib/ur/top.urs @ 2152:2d9e40e726f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Adjust new [assert] to work properly from top.ur
author Adam Chlipala <adam@chlipala.net>
date Wed, 03 Jun 2015 09:55:37 -0400
parents a3435112b83e
children 9029e0e2c67c
comparison
equal deleted inserted replaced
2151:4cd36865e0b5 2152:2d9e40e726f2
33 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1 33 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
34 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2 34 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
35 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3 35 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
36 36
37 (* Convert a record of n Units into a type-level record where 37 (* Convert a record of n Units into a type-level record where
38 each field has the same value (which describes a uniformly 38 o each field has the same value (which describes a uniformly
39 typed record) *) 39 typed record) *)
40 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f) 40 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
41 41
42 (* Existential type former *) 42 (* Existential type former *)
43 con ex :: K --> (K -> Type) -> Type 43 con ex :: K --> (K -> Type) -> Type
288 288
289 val postFields : postBody -> list (string * string) 289 val postFields : postBody -> list (string * string)
290 290
291 val max : t ::: Type -> ord t -> t -> t -> t 291 val max : t ::: Type -> ord t -> t -> t -> t
292 val min : t ::: Type -> ord t -> t -> t -> t 292 val min : t ::: Type -> ord t -> t -> t -> t
293
294 val assert : t ::: Type
295 -> bool (* Did we avoid something bad? *)
296 -> string (* Explanation of the bad thing *)
297 -> string (* Source location of the bad thing *)
298 -> t (* Return this value if all went well. *)
299 -> t