Fix
This commit is contained in:
parent
e598170ab3
commit
eab6907624
@ -774,7 +774,7 @@ This builds a search tree over multiple possible solutions.
|
|||||||
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a}\\
|
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a}\\
|
||||||
\hline
|
\hline
|
||||||
\wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a},
|
\wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a},
|
||||||
\tv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}},
|
\ntv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}},
|
||||||
%\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
|
%\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
|
||||||
\overline{\tv{u} \lessdot \type{S}}
|
\overline{\tv{u} \lessdot \type{S}}
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user