You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<h3><spanclass="math notranslate nohighlight">\(\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)</span><aclass="headerlink" href="#id1" title="Permalink to this heading">¶</a></h3>
549
549
<ulclass="simple">
550
550
<li><p>The type <spanclass="math notranslate nohighlight">\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\)</span> must be defined in the context.</p></li>
551
-
<li><p>Then <spanclass="math notranslate nohighlight">\(\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)</span> elaborates to <spanclass="math notranslate nohighlight">\(\href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\)</span>.</p></li>
551
+
<li><p>Then the type bound <spanclass="math notranslate nohighlight">\(\href{../syntax/types.html#syntax-typebound}{\mathsf{EQ}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)</span> elaborates to
<spanid="id2"></span><h2>Extern descriptors<aclass="headerlink" href="#extern-descriptors" title="Permalink to this heading">¶</a></h2>
763
+
<h2>Extern descriptors<aclass="headerlink" href="#extern-descriptors" title="Permalink to this heading">¶</a></h2>
763
764
<p>An extern descriptor elaborates to a quantified <spanclass="math notranslate nohighlight">\(\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\)</span>
<h3>Notational conventions<aclass="headerlink" href="#id3" title="Permalink to this heading">¶</a></h3>
868
+
<sectionid="id2">
869
+
<h3>Notational conventions<aclass="headerlink" href="#id2" title="Permalink to this heading">¶</a></h3>
869
870
<ulclass="simple">
870
871
<li><p>Much like with instance types above, we write <spanclass="math notranslate nohighlight">\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
871
872
\oplus \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}'\)</span> to mean the combination of two component
@@ -902,8 +903,8 @@ <h3>Notational conventions<a class="headerlink" href="#id3" title="Permalink to
902
903
\begin{array}{@{}c@{}}
903
904
\mathrm{defined}(\alpha) =
904
905
\begin{cases}
905
-
\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e} & \text{if } \exists i, \alpha_i = \alpha \land {\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}}^\alpha_i = \href{../syntax/types.html#syntax-typebound}{\mathsf{EQ}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\def\mathdef1#1{{}}\mathdef1{(ecoreinstancetype)} & \href{../valid/types.html#syntax-ecoreinstancetype}{\mathit{core{:}instancetype}_e} &::=&
<h3>Notational conventions<aclass="headerlink" href="#id5" title="Permalink to this heading">¶</a></h3>
1111
+
<sectionid="id4">
1112
+
<h3>Notational conventions<aclass="headerlink" href="#id4" title="Permalink to this heading">¶</a></h3>
1112
1113
<ulclass="simple">
1113
1114
<li><p>Much like with core instance types above, we write
1114
1115
<spanclass="math notranslate nohighlight">\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e} \oplus \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}'\)</span> to mean the
0 commit comments