2. d2: Collection(dec())
3. rho: Decl
4. l: Label
5. u1: decl_type([[d1]] rho;l)
6. d1 = d2
u1 
[[dec_lookup(d2;l)]] rho 
d1,d2:Collection(dec()), rho:Decl, u:(
[[d1]] rho). d1 = d2 
u ([[d2]] rho)da:Collection(dec()), rho:Decl, k:Label
, w:[[dec_lookup(da;k)]] rho. < k,w > ([[da]] rho)| 1 | 1. d1: Collection(dec()) 2. d2: Collection(dec()) 3. rho: Decl 4. l: Label 5. u1: decl_type([[d1]] rho;l) 6. d1 = d2 u1 [[dec_lookup(d2;l)]] rho |
About:
 |  |  |