comparison src/elab_util.sig @ 329:eec65c11d3e2

foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents e86411f647c6
children 85819353a84f
comparison
equal deleted inserted replaced
328:58f1260f293f 329:eec65c11d3e2
36 end 36 end
37 37
38 structure Con : sig 38 structure Con : sig
39 datatype binder = 39 datatype binder =
40 Rel of string * Elab.kind 40 Rel of string * Elab.kind
41 | Named of string * Elab.kind 41 | Named of string * int * Elab.kind
42 42
43 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 43 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
44 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 44 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
45 bind : 'context * binder -> 'context} 45 bind : 'context * binder -> 'context}
46 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB 46 -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB
60 end 60 end
61 61
62 structure Exp : sig 62 structure Exp : sig
63 datatype binder = 63 datatype binder =
64 RelC of string * Elab.kind 64 RelC of string * Elab.kind
65 | NamedC of string * Elab.kind 65 | NamedC of string * int * Elab.kind
66 | RelE of string * Elab.con 66 | RelE of string * Elab.con
67 | NamedE of string * Elab.con 67 | NamedE of string * Elab.con
68 68
69 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 69 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
70 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 70 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
86 end 86 end
87 87
88 structure Sgn : sig 88 structure Sgn : sig
89 datatype binder = 89 datatype binder =
90 RelC of string * Elab.kind 90 RelC of string * Elab.kind
91 | NamedC of string * Elab.kind 91 | NamedC of string * int * Elab.kind
92 | Str of string * Elab.sgn 92 | Str of string * Elab.sgn
93 | Sgn of string * Elab.sgn 93 | Sgn of string * Elab.sgn
94 94
95 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, 95 val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
96 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 96 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
115 end 115 end
116 116
117 structure Decl : sig 117 structure Decl : sig
118 datatype binder = 118 datatype binder =
119 RelC of string * Elab.kind 119 RelC of string * Elab.kind
120 | NamedC of string * Elab.kind 120 | NamedC of string * int * Elab.kind
121 | RelE of string * Elab.con 121 | RelE of string * Elab.con
122 | NamedE of string * Elab.con 122 | NamedE of string * Elab.con
123 | Str of string * Elab.sgn 123 | Str of string * Elab.sgn
124 | Sgn of string * Elab.sgn 124 | Sgn of string * Elab.sgn
125 125