Mercurial > urweb
annotate tests/modproj.lac @ 82:b4f2a258e52c
Initial disjointness prover
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 10:55:38 -0400 |
parents | 02f42e9a1825 |
children |
rev | line source |
---|---|
adamc@35 | 1 signature S1 = sig |
adamc@34 | 2 type t |
adamc@34 | 3 val zero : t |
adamc@34 | 4 end |
adamc@35 | 5 signature S2 = sig |
adamc@35 | 6 type t = int |
adamc@35 | 7 val zero : t |
adamc@35 | 8 end |
adamc@35 | 9 structure S = struct |
adamc@34 | 10 type t = int |
adamc@34 | 11 val zero = 0 |
adamc@34 | 12 end |
adamc@35 | 13 structure S1 : S1 = S |
adamc@35 | 14 structure S2 : S2 = S |
adamc@34 | 15 |
adamc@35 | 16 type t = S1.t |
adamc@35 | 17 val zero : t = S1.zero |
adamc@35 | 18 |
adamc@35 | 19 type t = S2.t |
adamc@35 | 20 val zero : int = S2.zero |
adamc@35 | 21 |
adamc@35 | 22 structure T = S1 |
adamc@39 | 23 val main : S1.t = T.zero |