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