Mercurial > urweb
comparison lib/ur/top.urs @ 2152:2d9e40e726f2
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 |