annotate tests/sig_impl.ur @ 1207:ae3036773768

Introduced the known() predicate
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Apr 2010 09:51:36 -0400
parents 71bafe66dbe1
children
rev   line source
adamc@78 1 signature S = sig
adamc@78 2 type t
adamc@78 3 val x : t
adamc@78 4 end
adamc@78 5
adamc@78 6 structure M : S = struct
adamc@78 7 val x = 0
adamc@78 8 end
adamc@78 9
adamc@78 10 signature S = sig
adamc@78 11 con r :: {Type}
adamc@78 12 val x : $r
adamc@78 13 end
adamc@78 14
adamc@78 15 structure M : S = struct
adamc@78 16 val x = {A = 0, B = "Hi"}
adamc@78 17 end
adamc@78 18
adamc@78 19 signature S = sig
adamc@78 20 type t
adamc@78 21 con r :: {Type}
adamc@78 22 val x : t -> $r
adamc@78 23 end
adamc@78 24
adamc@78 25 structure M : S = struct
adamc@78 26 val x = fn v : int => {A = 0, B = "Hi"}
adamc@78 27 end
adamc@79 28
adamc@79 29 signature S = sig
adamc@79 30 con nm :: Name
adamc@79 31 con t :: Type
adamc@79 32 con r :: {Type}
adamc@79 33 val x : $([nm = t] ++ r)
adamc@79 34 end
adamc@79 35
adamc@79 36 structure M : S = struct
adamc@79 37 val x = {A = 0, B = "Hi"}
adamc@79 38 end
adamc@79 39
adamc@79 40 signature S = sig
adamc@79 41 con nm :: Name
adamc@79 42 con r :: {Type}
adamc@79 43 val x : $([nm = int] ++ r)
adamc@79 44 end
adamc@79 45
adamc@79 46 structure M : S = struct
adamc@79 47 val x = {A = 0, B = "Hi"}
adamc@79 48 end
adamc@79 49
adamc@79 50 signature S = sig
adamc@79 51 con nm :: Name
adamc@79 52 con r :: {Type}
adamc@79 53 val x : $([nm = string] ++ r)
adamc@79 54 end
adamc@79 55
adamc@79 56 structure M : S = struct
adamc@79 57 val x = {A = 0, B = "Hi"}
adamc@79 58 end