Mercurial > urweb
annotate tests/disjoint.lac @ 84:e86370850c30
Disjointness assumptions
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 01 Jul 2008 12:10:46 -0400 |
| parents | 0a1baddd8ab2 |
| children | 1f85890c9846 |
| rev | line source |
|---|---|
| adamc@84 | 1 con c1 = fn x :: Name => [x] ~ [A] => [x, A] |
| adamc@84 | 2 con c2 = fn x :: Name => [x] ~ [A] => [A, x] |
| adamc@84 | 3 con c3 = fn x :: Name => [A] ~ [x] => [x, A] |
| adamc@84 | 4 con c4 = fn x :: Name => [A] ~ [x] => [A, x] |
| adamc@84 | 5 |
| adamc@84 | 6 con c5 = fn r1 :: {Type} => fn r2 => r1 ~ r2 => r1 ++ r2 |
| adamc@84 | 7 con c6 = fn r1 :: {Type} => fn r2 => r2 ~ r1 => r1 ++ r2 |
| adamc@84 | 8 |
| adamc@84 | 9 con c7 = fn x :: Name => fn r => [x] ~ r => [x] ++ r |