<commit_before>\documentclass{article}

\usepackage{amsmath,amssymb}
\usepackage{mathpartir}

\newcommand{\Type}{\mathsf{Type}}
\newcommand{\ctx}{\Gamma}
\newcommand{\emptyctx}{\cdot}
\newcommand{\evalto}{\Longrightarrow}

\newcommand{\jdg}[3]{#1 : (#2) \; . \, #3}
\newcommand{\isfresh}[1]{\mathsf{fresh}\;#1}

\newcommand{\prd}[1]{\Pi #1 \,.\,}
\newcommand{\Eq}[3][]{#2 \equiv_{#1} #3}
\newcommand{\refl}[2][]{\mathsf{refl}_{#1}\,#2}
\newcommand{\fun}[1]{\lambda #1 \,.\,}
\newcommand{\abs}[1]{#1 \,.\,}
\newcommand{\app}[3][]{#2 \mathrel{@}^{#1} #3}

\newcommand{\anon}{\_}

\newcommand{\join}{\bowtie}
\newcommand{\splitctx}{\rightsquigarrow}

\begin{document}

\begin{mathpar}
  \infer[eval-Type]
  { }
  {\Type \evalto \jdg{\Type}{\emptyctx}{\Type}}

  \infer[eval-Var]
  { \isfresh{\alpha}}
  { x \evalto \jdg{x}{\alpha : \Type, x : \alpha}{\alpha}}

  \infer[eval-Prod]
  {
  c_1 \evalto \jdg{e_1}{\ctx_1}{A_1} \\
  c_2 \evalto \jdg{e_2}{\ctx_2}{A_2} \\
  \ctx_2 \splitctx (\ctx'_2, x : B, \Delta)
  }
  {
  \begin{aligned}
  &\prd{x : c_1} c_2
  \evalto
  \jdg
    {\prd{x : e_1} e_2}
    {\\&(\ctx_1 \join \ctx'_2) +
     (\anon : \Eq[\Type]{A_1}{\Type}) +
     (\anon : \prd{x : B} \Eq[\Type]{A_2}{\Type}) +
     (\anon : \Eq[\Type]{e_1}{B}) +
     (\prd{x : B} \Delta)
    }{
     \Type
    }
  \end{aligned}
  }

  \infer[eval-Eq]
  {
    c_1 \evalto \jdg{e_1}{\ctx_1}{A_1} \\
    c_2 \evalto \jdg{e_2}{\ctx_2}{A_2} \\
    \isfresh{\alpha}
  }{
    \Eq{c_1}{c_2}
    \evalto
    \jdg
    {
      \Eq[\alpha]{e_1}{e_2}
    }{
      (\ctx_1 \join \ctx_2) +
      (\alpha : \Type) +
      (\anon : \Eq[\Type]{\alpha}{A_1}) +
      (\anon : \Eq[\Type]{\alpha}{A_1})
    }{
      \Type
    }
  }

  \infer[eval-Refl]
  {c \evalto \jdg{e}{\ctx}{A}}
  {\refl{c}
   \evalto
   \jdg
   {\refl[A]{e}}
   {\ctx}
   {\Eq[A]{e}{e}}
  }

  \infer[eval-Fun]
  {c \evalto \jdg{e}{\ctx}{A} \\
   \ctx \splitctx (\ctx', x : B, \Delta)
  }{
    \fun{x} c
    \evalto
    \jdg
    {\fun{x:B}{e}}
    {\ctx' + (\prd{x:B} \Delta)}
    {\prd{x : B} A}
  }

  \infer[eval-App]
  {
   c_1 \evalto \jdg{e_1}{\ctx_1}{A_1} \\
   c_2 \evalto \jdg{e_2}{\ctx_2}{A_2} \\
   \isfresh{\alpha}
  }
  {
  \begin{aligned}
   &\app{c_1}{c_2}
   \evalto
   \jdg
   {
    \app[\abs{x : \alpha} {\app[\abs{\anon : \alpha} \Type]{\beta}{x}}]{e_1}{e_2}
   }{
    \\&(\ctx_1 \join \ctx_2) +
    (\alpha : \Type) +
    (\beta : \alpha \to \Type) +
    (\anon : \Eq[\Type]{\alpha}{A_2}) +
    (\prd{x : \alpha} \Eq[\Type]{\app[\abs{\anon : \alpha} \Type]{\beta}{x}}{A_1})
   }{
    \app[\abs{\anon : \alpha} \Type]{\beta}{e_2}
   }
  \end{aligned}
  }


\end{mathpar}
\end{document}<commit_msg>Typos and formatting<commit_after>\documentclass{article}

\usepackage{amsmath,amssymb}
\usepackage{mathpartir}

\newcommand{\Type}{\mathsf{Type}}
\newcommand{\ctx}{\Gamma}
\newcommand{\emptyctx}{\cdot}
\newcommand{\evalto}{\Longrightarrow}

\newcommand{\jdg}[3]{#1 : #3 \; \left[#2\right]}
\newcommand{\isfresh}[1]{\mathsf{fresh}\;#1}

\newcommand{\prd}[1]{\Pi #1 \,.\,}
\newcommand{\Eq}[3][]{#2 \equiv_{#1} #3}
\newcommand{\refl}[2][]{\mathsf{refl}_{#1}\,#2}
\newcommand{\fun}[1]{\lambda #1 \,.\,}
\newcommand{\abs}[1]{#1 \,.\,}
\newcommand{\app}[3][]{#2 \mathrel{@}^{#1} #3}

\newcommand{\anon}{\_}

\newcommand{\join}{\bowtie}
\newcommand{\splitctx}{\rightsquigarrow}

\begin{document}

\begin{mathpar}
  \infer[eval-Type]
  { }
  {\Type \evalto \jdg{\Type}{\emptyctx}{\Type}}

  \infer[eval-Var]
  { \isfresh{\alpha}}
  { x \evalto \jdg{x}{\alpha : \Type, x : \alpha}{\alpha}}

  \infer[eval-Prod]
  {
  c_1 \evalto \jdg{e_1}{\ctx_1}{A_1} \\
  c_2 \evalto \jdg{e_2}{\ctx_2}{A_2} \\
  \ctx_2 \splitctx (\ctx'_2, x : B, \Delta)
  }
  {
  \prd{x : c_1} c_2
  \evalto
  \jdg
    {\prd{x : e_1} e_2}
    {\begin{aligned}
     & (\ctx_1 \join \ctx'_2) +
       (\anon : \Eq[\Type]{A_1}{\Type}) + \\
     & (\anon : \prd{x : B} (\Eq[\Type]{A_2}{\Type})) +
       (\anon : \Eq[\Type]{e_1}{B}) +
       (\prd{x : B} \Delta)
     \end{aligned}
    }{
     \Type
    }
  }

  \infer[eval-Eq]
  {
    c_1 \evalto \jdg{e_1}{\ctx_1}{A_1} \\
    c_2 \evalto \jdg{e_2}{\ctx_2}{A_2} \\
    \isfresh{\alpha}
  }{
    \Eq{c_1}{c_2}
    \evalto
    \jdg
    {
      \Eq[\alpha]{e_1}{e_2}
    }{
      (\ctx_1 \join \ctx_2) +
      (\alpha : \Type) +
      (\anon : \Eq[\Type]{\alpha}{A_1}) +
      (\anon : \Eq[\Type]{\alpha}{A_2})
    }{
      \Type
    }
  }

  \infer[eval-Refl]
  {c \evalto \jdg{e}{\ctx}{A}}
  {\refl{c}
   \evalto
   \jdg
   {\refl[A]{e}}
   {\ctx}
   {(\Eq[A]{e}{e})}
  }

  \infer[eval-Fun]
  {c \evalto \jdg{e}{\ctx}{A} \\
   \ctx \splitctx (\ctx', x : B, \Delta)
  }{
    (\fun{x} c)
    \evalto
    \jdg
    {(\fun{x:B}{e})}
    {\ctx' + (\prd{x:B} \Delta)}
    {(\prd{x : B} A)}
  }

  \infer[eval-App]
  {
   c_1 \evalto \jdg{e_1}{\ctx_1}{A_1} \\
   c_2 \evalto \jdg{e_2}{\ctx_2}{A_2} \\
   \isfresh{\alpha}
  }
  {
   \app{c_1}{c_2}
   \evalto
   \jdg
   {
    \app[\abs{x : \alpha} {\app[\abs{\anon : \alpha} \Type]{\beta}{x}}]{e_1}{e_2}
   }{
    \begin{aligned}
    & (\ctx_1 \join \ctx_2) +
      (\alpha : \Type) +
      (\beta : \alpha \to \Type) + \\
    & (\anon : \Eq[\Type]{\alpha}{A_2}) + \\
    & (\prd{x : \alpha} (\Eq[\Type]{\app[\abs{\anon : \alpha} \Type]{\beta}{x}}{A_1}))
    \end{aligned}
   }{
    \app[\abs{\anon : \alpha} \Type]{\beta}{e_2}
   }
  }


\end{mathpar}
\end{document}
{'fraction_non_alphanumeric': 0.2785422089996281, 'fraction_numerical': 0.027891409445890667, 'mean_word_length': 2.293937538273117, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '755068', 'n_tokens_mistral': 2551, 'n_tokens_neox': 2494, 'n_words': 341}