1 | 1. x: SimpleType 2. r1: Term List 3. ds: Collection(dec()) 4. da: Collection(dec()) 5. de: sig() 6. rho: Decl 7. st1: Collection(SimpleType) 8. e: {[[de]] rho} 9. s: {[[ds]] rho} 10. a: [[st1]] rho 11. tr: trace_env([[da]] rho) 12. trace_consistent_rel(rho;da;tr.proj; < inl(x),r1 > ) 13. l: Term List 14. r1 = l 15. ||l|| = 2 ![]() ![]() 16. x ![]() 17. x ![]() ![]() ![]() |
2 | 1. y: Label 2. r1: Term List 3. ds: Collection(dec()) 4. da: Collection(dec()) 5. de: sig() 6. rho: Decl 7. st1: Collection(SimpleType) 8. e: {[[de]] rho} 9. s: {[[ds]] rho} 10. a: [[st1]] rho 11. tr: trace_env([[da]] rho) 12. trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > ) 13. l: Term List 14. r1 = l 15. ||de.rel(y)|| = ||l|| ![]() ![]() 16. ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 1. y: Label 2. r1: Term List 3. ds: Collection(dec()) 4. da: Collection(dec()) 5. de: sig() 6. rho: Decl 7. st1: Collection(SimpleType) 8. e: {[[de]] rho} 9. s: {[[ds]] rho} 10. a: [[st1]] rho 11. tr: trace_env([[da]] rho) 12. trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > ) 13. l: Term List 14. r1 = l ![]() ![]() |
4 | 1. y: Label 2. r1: Term List 3. ds: Collection(dec()) 4. da: Collection(dec()) 5. de: sig() 6. rho: Decl 7. st1: Collection(SimpleType) 8. e: {[[de]] rho} 9. s: {[[ds]] rho} 10. a: [[st1]] rho 11. tr: trace_env([[da]] rho) 12. trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > ) 13. l: Term List 14. r1 = l ![]() ![]() |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |