Ur/Web: tests/functor.lac annotate

Initial disjointness prover

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 01 Jul 2008 10:55:38 -0400
parents	ac4c0b4111ba
children

rev	line source
adamc@40	1 signature S = sig
adamc@40	2 type t
adamc@40	3 val z : t
adamc@40	4 val s : t -> t
adamc@40	5 end
adamc@40	6
adamc@40	7 signature T = sig
adamc@40	8 type t
adamc@40	9 val three : t
adamc@40	10 end
adamc@40	11
adamc@42	12 functor F (M : S) : T where type t = M.t = struct
adamc@41	13 type t = M.t
adamc@40	14 val three = M.s (M.s (M.s M.z))
adamc@40	15 end
adamc@43	16
adamc@44	17
adamc@44	18 structure O = F (struct
adamc@44	19 type t = int
adamc@44	20 val z = 0
adamc@44	21 val s = fn x : t => x
adamc@44	22 end)
adamc@44	23 val three : int = O.three
adamc@44	24
adamc@44	25 structure S = struct
adamc@44	26 type t = int
adamc@44	27 val z = 0
adamc@44	28 val s = fn x : t => x
adamc@44	29 end
adamc@44	30 structure SO = F (S)
adamc@44	31 val three : int = SO.three
adamc@44	32
adamc@44	33 structure SS : S = S
adamc@44	34 structure SSO = F (SS)
adamc@44	35 val three : SS.t = SSO.three
adamc@47	36
adamc@47	37 val main = three

Mercurial > urweb