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 |