view tests/type_classMod.ur @ 1215:360f1ed0a969

Implemented proper congruence closure, to the point where tests/policy works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 08 Apr 2010 12:46:21 -0400
parents 71bafe66dbe1
children
line wrap: on
line source
structure M = struct
        structure N = struct
                class c t = t
                val string_c : c string = "Hi"
        end
end

val c : t :: Type -> M.N.c t -> t =
        fn t :: Type => fn pf : M.N.c t => pf
val hi = c [string] _

val bool_c : M.N.c bool = True
val true = c [bool] _
val hi = c [string] _

con c = M.N.c
val int_c : c int = 0
val zero = c [int] _