comparison src/elab_util.sig @ 1795:d28adceef22a

Allow type class instances with hypotheses via local ('let') definitions
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 14:04:59 -0400
parents 4a03aa3251cb
children 1091227f535a
comparison
equal deleted inserted replaced
1794:4671afac15af 1795:d28adceef22a
110 bind : 'context * binder -> 'context} 110 bind : 'context * binder -> 'context}
111 -> 'context -> (Elab.exp -> Elab.exp) 111 -> 'context -> (Elab.exp -> Elab.exp)
112 val exists : {kind : Elab.kind' -> bool, 112 val exists : {kind : Elab.kind' -> bool,
113 con : Elab.con' -> bool, 113 con : Elab.con' -> bool,
114 exp : Elab.exp' -> bool} -> Elab.exp -> bool 114 exp : Elab.exp' -> bool} -> Elab.exp -> bool
115 val existsB : {kind : 'context * Elab.kind' -> bool,
116 con : 'context * Elab.con' -> bool,
117 exp : 'context * Elab.exp' -> bool,
118 bind : 'context * binder -> 'context}
119 -> 'context -> Elab.exp -> bool
115 120
116 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state, 121 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
117 con : 'context * Elab.con' * 'state -> 'state, 122 con : 'context * Elab.con' * 'state -> 'state,
118 exp : 'context * Elab.exp' * 'state -> 'state, 123 exp : 'context * Elab.exp' * 'state -> 'state,
119 bind : 'context * binder -> 'context} 124 bind : 'context * binder -> 'context}