andreinaku / SpyType

MIT License
0 stars 0 forks source link

extend substitution for BoundVarType over VarType #44

Open andreinaku opened 4 months ago

andreinaku commented 4 months ago
(T1 <= T2 + int) /\ (T1 <= float) => (T1 <= T2 + int) /\ (T1 <= float) /\ (T2 <= float)

or

((T1 <= T2 + int)[S]) && ((T1 <= float)[S]) => 
((T1 <= float + int)[S and T2 |-> float]) && ((T1 <= float)[S and T2 |-> float])