Re: [NTG-context] Unicode superscript and subscript parentheses as operators

28 Dec 2021


      
...
On 28 Dec 2021, at 23:03, Hans Hagen  wrote:
On 12/28/2021 10:53 PM, Hans Åberg wrote:
...
\starttext
Course-of-values induction:
  $$𝜞 ⊢ 𝑷(0); 𝜞, 𝒚 ≤ 𝒙 ⇒ 𝑷(𝒚) ⊢⁽𝒚⁾₍𝒙₎ 𝑷(s(𝒙)) ⊩ 𝜞 ⊢ 𝑷(𝒕)$$
\stoptext
stay away from $$ but use
\startformula
 𝜞 ⊢ 𝑷(0); 𝜞, 𝒚 ≤ 𝒙 ⇒ 𝑷(𝒚) ⊢⁽𝒚⁾₍𝒙₎ 𝑷(s(𝒙)) ⊩ 𝜞 ⊢ 𝑷(𝒕)
 \stopformula
Thanks, I am aware if that, but wrote it in a hurry. :-)