ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s,s':{[[ds]] rho} , e:{1of([[de]] rho)}, a:SimpleType, v:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent(rho;daa;tr.proj;t) a term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho

1

1. ds: Collection(dec()) 2. daa: Collection(dec()) 3. da: Collection(SimpleType) 4. de: sig() 5. rho: Decl 6. t: Term s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent(rho;daa;tr.proj;t) a term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho

About: