Mercurial > urweb
annotate tests/type_classMod2.ur @ 1034:a779402841f6
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@218 | 1 signature S = sig |
adamc@218 | 2 class c |
adamc@218 | 3 val default : t :: Type -> c t -> t |
adamc@218 | 4 |
adamc@218 | 5 val string_c : c string |
adamc@218 | 6 val int_c : c int |
adamc@218 | 7 end |
adamc@218 | 8 |
adamc@218 | 9 structure M : S = struct |
adamc@218 | 10 class c t = t |
adamc@218 | 11 val default = fn t :: Type => fn v : c t => v |
adamc@218 | 12 |
adamc@218 | 13 val int_c : c int = 0 |
adamc@218 | 14 val string_c : c string = "Hi" |
adamc@218 | 15 end |
adamc@218 | 16 |
adamc@218 | 17 val hi = M.default [string] _ |
adamc@218 | 18 val zero = M.default [int] _ |