search

andreinaku / SpyType

MIT License
0 stars 0 forks source link

bug in orsubst with same left operand #45

Open andreinaku opened 4 months ago

andreinaku commented 4 months ago 
eq orsubst(S:Subst, S':Subst) = S:Subst, S':Subst [owise] .
S:Subst --> (T1 |-> str), (T2 |-> str), T4 |-> str
S':Subst --> (T2 |-> float), T4 |-> float
orsubst((T2 |-> float), T4 |-> float, (T1 |-> str), (T2 |-> str), T4 |-> str)