ds:Collection(dec()), rho:Decl, a:(
[[ds]] rho).
value(a) 
[[dec_lookup(ds;kind(a))]] rhods:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x)
, a:SimpleType. mk_dec(x, a) ds 
y [[a]] rho| Theorem | Name |
|
Thm* ds:Collection(dec()), rho:Decl, a:([[ds]] rho).
value(a) [[dec_lookup(ds;kind(a))]] rho | [sigma_decls_mng_value] |
| cites | |
|
Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x)
, a:SimpleType. mk_dec(x, a) ds y [[a]] rho | [decls_mng_subtype] |