Mercurial > urweb
comparison lib/ur/top.urs @ 2159:9029e0e2c67c
Stray character in a comment
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 04 Jul 2015 18:44:52 -0400 |
parents | 2d9e40e726f2 |
children |
comparison
equal
deleted
inserted
replaced
2158:b90103106177 | 2159:9029e0e2c67c |
---|---|
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 o each field has the same value (which describes a uniformly | 38 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 |