Mercurial > urweb
comparison src/elab.sml @ 82:b4f2a258e52c
Initial disjointness prover
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 10:55:38 -0400 |
parents | 522f4bd3955e |
children | e86370850c30 |
comparison
equal
deleted
inserted
replaced
81:60d97de1bbe8 | 82:b4f2a258e52c |
---|---|
32 datatype kind' = | 32 datatype kind' = |
33 KType | 33 KType |
34 | KArrow of kind * kind | 34 | KArrow of kind * kind |
35 | KName | 35 | KName |
36 | KRecord of kind | 36 | KRecord of kind |
37 | KUnit | |
37 | 38 |
38 | KError | 39 | KError |
39 | KUnif of ErrorMsg.span * string * kind option ref | 40 | KUnif of ErrorMsg.span * string * kind option ref |
40 | 41 |
41 withtype kind = kind' located | 42 withtype kind = kind' located |
58 | CName of string | 59 | CName of string |
59 | 60 |
60 | CRecord of kind * (con * con) list | 61 | CRecord of kind * (con * con) list |
61 | CConcat of con * con | 62 | CConcat of con * con |
62 | CFold of kind * kind | 63 | CFold of kind * kind |
64 | |
65 | CUnit | |
63 | 66 |
64 | CError | 67 | CError |
65 | CUnif of ErrorMsg.span * kind * string * con option ref | 68 | CUnif of ErrorMsg.span * kind * string * con option ref |
66 | 69 |
67 withtype con = con' located | 70 withtype con = con' located |