Mercurial > urweb

annotate tests/type_classMod.ur @ 1215:360f1ed0a969

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
rev   line source
adamc@217 1 structure M = struct
adamc@217 2 structure N = struct
adamc@217 3 class c t = t
adamc@217 4 val string_c : c string = "Hi"
adamc@217 5 end
adamc@217 6 end
adamc@217 7
adamc@217 8 val c : t :: Type -> M.N.c t -> t =
adamc@217 9 fn t :: Type => fn pf : M.N.c t => pf
adamc@217 10 val hi = c [string] _
adamc@217 11
adamc@217 12 val bool_c : M.N.c bool = True
adamc@217 13 val true = c [bool] _
adamc@217 14 val hi = c [string] _
adamc@217 15
adamc@217 16 con c = M.N.c
adamc@217 17 val int_c : c int = 0
adamc@217 18 val zero = c [int] _