Mercurial > urweb

annotate tests/type_classMod.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
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] _