macros.ts

<TeXmacs|2.1.1>

<style|source>

<\body>
  <\active*>
    <\src-title>
      <src-style-file|texmacs-macros|1.0>

      <src-purpose|Automatically generated style file.>
    </src-title>
  </active*>

  <use-package|article|indent-paragraphs|cite-author-year|comment>

  <\active*>
    <\src-comment>
      Style parameters.
    </src-comment>
  </active*>

  <assign|font|typewriter=roman,Linux Libertine>

  <assign|font-family|rm>

  <assign|full-screen-mode|false>

  <assign|info-flag|minimal>

  <assign|magnification|1>

  <assign|page-bot|4cm>

  <assign|page-even|4cm>

  <assign|page-medium|paper>

  <assign|page-odd|4cm>

  <assign|page-right|4cm>

  <assign|page-top|4cm>

  <assign|src-close|repeat>

  <assign|src-special|normal>

  <assign|src-style|angular>

  <\active*>
    <\src-comment>
      Macro definitions.
    </src-comment>
  </active*>

  <assign|doi|<macro|id|<slink|https://doi.org/<arg|id>>>>

  <assign|of|<macro|x|A|<math|<arg|x> : <arg|A>>>>

  <assign|def-emph|<macro|x|<with|font-series|bold|<with|font-shape|italic|<arg|x>>>>>

  <\active*>
    \;
  </active*>

  <assign|kwd|<macro|x|<math|<math-bf|<arg|x>>>>>

  <assign|con|<macro|x|<math|<math-ss|<arg|x>>>>>

  <assign|concr|<macro|x|<math|<math-tt|<arg|x>>>>>

  \;

  <assign|abs|<macro|x|bdy|<math|\<lambda\><arg|x>.<space|0.2spc><arg|bdy>>>>

  \;

  <assign|kwd-begin|<macro|<kwd|begin>>>

  <assign|kwd-end|<macro|<kwd|end>>>

  <assign|kwd-sig|<macro|<kwd|signature>>>

  <assign|kwd-def|<macro|<kwd|def>>>

  <assign|kwd-struct|<macro|<kwd|structure>>>

  <assign|arg-sep|<macro|<space|0.6spc>>>

  \;

  <assign|!nm|<macro|<concr|Name>>>

  <assign|!ctx|<macro|<concr|Ctx>>>

  <assign|!tp|<macro|<concr|Type>>>

  <assign|!ptm|<macro|<concr|Preterm>>>

  <assign|aeq|<macro|<math|\<equiv\><rsub|\<alpha\>>>>>

  <assign|quo|<macro|A|R|<math|<arg|A>/<arg|R>>>>

  \;

  <assign|!tp-arr|<macro|s|t|<math|<arg|s> \<Rightarrow\> <arg|t>>>>

  <assign|!tp-prod|<macro|s|t|<math|<arg|s> \<times\> <arg|t>>>>

  <assign|!tp-bool|<macro|<concr|bool>>>

  <assign|!tm-lam|<macro|x|s|M|<math|\<lambda\><arg|x><rsup|<arg|s>>.<space|0.2spc><arg|M>>>>

  <assign|!tm-true|<macro|<concr|true>>>

  <assign|!tm-false|<macro|<concr|false>>>

  \;

  <assign|STLC|<macro|univ|<math|<con|STLC><rsub|<arg|univ>>>>>

  <assign|ISTLC|<macro|univ|<math|<con|ISTLC><rsub|<arg|univ>>>>>

  \;

  <assign|UU|<macro|<math|<with|font|cal|U>>>>

  <assign|VV|<macro|<math|<with|font|cal|V>>>>

  <assign|triv|<macro|<math|\<star\>>>>

  <assign|obj-one|<macro|<kwd|1>>>

  <assign|obj-two|<macro|<kwd|2>>>

  <assign|inl*|<macro|inl>>

  <assign|inl|<macro|x|<inl*><arg-sep><arg|x>>>

  <assign|inr*|<macro|inr>>

  <assign|inr|<macro|x|<inr*><arg-sep><arg|x>>>

  \;

  <assign|sort-tp|<macro|<con|type>>>

  <assign|sort-tm*|<macro|<con|tm>>>

  <assign|sort-tm|<macro|tp|<sort-tm*> <arg|tp>>>

  <assign|sort-el*|<macro|<con|el>>>

  <assign|sort-el|<macro|tau|<sort-el*> <arg|tau>>>

  <assign|tp-arr*|<macro|<con|arr>>>

  <assign|tp-arr|<macro|sigma|tau|<tp-arr*><arg-sep><arg|sigma><arg-sep><arg|tau>>>

  <assign|tp-prod*|<macro|<con|prod>>>

  <assign|tp-prod|<macro|sigma|tau|<math|<tp-prod*><arg-sep><arg|sigma><arg-sep><arg|tau>>>>

  \;

  <assign|tm-lam*|<macro|<con|lam>>>

  <assign|tm-lam|<macro|bdy|<math|<tm-lam*><arg-sep><arg|bdy>>>>

  <assign|tm-app*|<macro|<con|app>>>

  <assign|tm-app|<macro|f|x|<math|<tm-app*><arg-sep><arg|f><arg-sep><arg|x>>>>

  <assign|tm-arr-beta|<macro|<math|<tp-arr*><rsub|\<beta\>>>>>

  <assign|tm-arr-eta|<macro|<math|<tp-arr*><rsub|\<eta\>>>>>

  \;

  <assign|tm-pair*|<macro|<con|pair>>>

  <assign|tm-pair|<macro|u|v|<math|<tm-pair*><arg-sep><arg|u><arg-sep><arg|v>>>>

  <assign|tm-fst*|<macro|<con|fst>>>

  <assign|tm-fst|<macro|u|<math|<tm-fst*><arg-sep><arg|u>>>>

  <assign|tm-snd*|<macro|<con|snd>>>

  <assign|tm-snd|<macro|u|<math|<tm-snd*><arg-sep><arg|u>>>>

  <assign|tm-prod-beta-fst|<macro|<math|<tp-prod*><rsub|\<beta\>1>>>>

  <assign|tm-prod-beta-snd|<macro|<math|<tp-prod*><rsub|\<beta\>2>>>>

  <assign|tm-prod-eta|<macro|<math|<tp-prod*><rsub|\<eta\>>>>>

  \;

  <assign|tp-bool|<macro|<con|bool>>>

  <assign|tm-true|<macro|<con|true>>>

  <assign|tm-false|<macro|<con|false>>>

  <assign|tm-case*|<macro|<con|case>>>

  <assign|tm-case|<macro|u|v|w|<math|<tm-case*><arg-sep><arg|u><arg-sep><arg|v><arg-sep><arg|w>>>>

  <assign|tm-bool-beta-true|<macro|<math|<tp-bool><rsub|\<beta\>1>>>>

  <assign|tm-bool-beta-false|<macro|<math|<tp-bool><rsub|\<beta\>2>>>>

  <assign|tm-bool-eta|<macro|<math|<tp-bool><rsub|\<eta\>>>>>

  \;

  <assign|emp-cx|<math|\<cdot\>>>

  \;

  <assign|obj-opn|<macro|<math|\<b-Phi\>>>>

  <assign|lobj-opn|<macro|<math|\<b-Phi\><rsub|<con|L>>>>>

  <assign|robj-opn|<macro|<math|\<b-Phi\><rsub|<con|R>>>>>

  <assign|l2r|<macro|<math|<around|[|\<looparrowright\>|]>>>>

  <assign|r2l|<macro|<math|<around|[|\<looparrowleft\>|]>>>>

  \;

  <assign|op-mod|<macro|p|u|<math|<hgroup|<arg|p>\<Rightarrow\><arg|u>>>>>

  <assign|obj|<macro|u|<op-mod|<obj-opn>|<arg|u>>>>

  <assign|lobj|<macro|u|<op-mod|<lobj-opn>|<arg|u>>>>

  <assign|robj|<macro|u|<op-mod|<robj-opn>|<arg|u>>>>

  \;

  <assign|meta|<macro|u|<math|<hgroup|<obj-opn>\<bullet\><arg|u>>>>>

  <assign|dep-meta|<macro|tele|u|<meta|<surround|[|]|<arg|tele>>. <arg|u>>>>

  <assign|meta-unit|<macro|<math|\<eta\><rsub|<obj-opn>\<bullet\>>>>>

  <assign|hookrightarrow|<macro|\<hookrightarrow\>>>

  \;

  <assign|compr|<macro|A|B|<math|<hgroup|<around*|{| <arg|A> <mid|\|> <arg|B>
  |}>>>>>

  <assign|ixfam|<macro|A|B|<math|<hgroup|<around*|(| <arg|A> <mid|\|> <arg|B>
  |)>>>>>

  <assign|ext|<macro|A|prop|a|<math|<compr|<arg|A>|<arg|prop><hookrightarrow><arg|a>>>>>

  <assign|obj-ext|<macro|A|a|<ext|<arg|A>|<obj-opn>|<arg|a>>>>

  <assign|refine|<macro|opn|x|A|Bx|<math|<hgroup|<around*|[|<arg|opn><hookrightarrow><of|<arg|x>|<arg|A>>
  <mid|\|> <arg|Bx>|]>>>>>

  <assign|refine-el|<macro|opn|a|b|<math|<hgroup|<around*|[|<arg|opn><hookrightarrow><arg|a>
  <mid|\|> <arg|b>|]>>>>>

  \;

  <assign|coloneq|<macro|<math|\<assign\>>>>

  \;

  <assign|M|<macro|<con|M>>>

  <assign|M*|<macro|<math|<M><rprime|\<asterisk\>>>>>

  <assign|N|<macro|<con|N>>>

  <assign|interp|<macro|model|term|<active*|<compound|math|>><math|<surround|\<llbracket\>|\<rrbracket\>|<arg|term>><rsup|<arg|model>>>>>

  \;

  <assign|em-abbr|<macro|x|<abbr|<em|<arg|x>>>>>

  <assign|ie|<macro|<em-abbr|i.e.>>>

  <assign|eg|<macro|<em-abbr|e.g.>>>

  <assign|etc|<macro|<em-abbr|etc.>>>

  \;

  <assign|is-ctx|<macro|G|<math|<arg|G><arg-sep><text|<with|font-shape|italic|ctx>>>>>

  <assign|is-tp|<macro|A|<math|<arg|A><arg-sep><text|<with|font-shape|italic|type>>>>>

  <assign|is-tm|<macro|G|M|A|<math|<arg|G> \<vdash\> <of|<arg|M>|<arg|A>>>>>

  <assign|eq-tm|<macro|G|M|N|A|<is-tm|<arg|G>|<arg|M> \<equiv\>
  <arg|N>|<arg|A>>>>

  \;

  <assign|unrefine|<macro|u|<underline|<arg|u>>>>

  <assign|hole|<macro|idn|<math|<with|color|red|?<rsub|<arg|idn>>>>>>

  \;

  <assign|postulate-box|<macro|body|<with|padding-below|1fn|padding-above|1fn|framed-color|pastel
  magenta|<\framed>
    <arg|body>
  </framed>>>>

  \;

  <assign|rulebox|<\macro|body>
    <padded-center|<arg|body>>
  </macro>>

  \;

  <assign|infer|<\macro|upstairs|downstairs>
    <\math>
      <below|<above|<surround|<space|2em>|<space|2em>|<dfrac|<arg|upstairs>|<arg|downstairs>>>|<vspace|.5fn>>|<vspace|.5fn>>
    </math>
  </macro>>

  \;

  <assign|arr-id|<macro|G|<kwd|id><rsub|<arg|G>>>>

  \;

  <assign|ob|<macro|C|<math|ob <arg|C>>>>

  <assign|flech*|<macro|C|<math|hom<rsub|<arg|C>>>>>

  <assign|flech|<macro|C|x|y|<math|<compound|flech*|<arg|C>><surround|(|)|<arg|x>,<arg|y>>>>>

  \;

  <assign|ccat|<macro|<with|font|cal|C>>>

  <assign|dcat|<macro|<with|font|cal|D>>>

  <assign|ecat|<macro|<with|font|cal|E>>>

  \;

  <assign|SET|<macro|<kwd|Set>>>

  <assign|yo|<macro|C|<math|<con|y><rsub|<arg|C>>>>>

  <assign|psh|<macro|C|<math|<kwd|Pr> <arg|C>>>>

  <assign|op-cat|<macro|C|<math|<arg|C><rsup|<con|op>>>>>

  <assign|syn-cat|<macro|<with|font|Bbb|T>>>

  <assign|gsec|<macro|<math|<kwd|\<Gamma\>>>>>

  \;

  <new-remark|computation|Computation>

  <new-remark|intuition|Intuition>

  <new-remark|construction|Construction>

  <new-remark|postulate|Postulate>

  \;

  <assign|by-text|<macro|>>

  <assign|doc-title|<macro|x|<\surround|<vspace*|0.5fn>|<vspace|0.5fn>>
    <doc-title-block|<font-magnify|1.5|<doc-title-name|<arg|x>>>>
  </surround>>>

  \;

  <assign|ospace|<macro|object-space>>

  <assign|mspace|<macro|meta-space>>
</body>

<\initial>
  <\collection>
    <associate|preamble|true>
  </collection>
</initial>