Mercurial > urweb
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 |