rules.tex

\begin{trules}{Higher-Order Patterns}{coucou}
  \rrulep{}{c \in \Gamma}{\jwpat{\Gamma;\Delta}{c}}

  \rrulepp{}{\jwpat{\Gamma;\Delta}{t}}{\jwpatpho{\Gamma;\Delta;\emptyset}{u}}{\jwpat{\Gamma;\Delta}{\tapp{t}{u}}}
 
  \rrulep{}{x \in \Gamma \cup \Xi}{\jwpatpho{\Gamma;\Delta;\Xi}{x}}
  
  \rrulep{}{\jwpatpho{\Gamma;\Delta;\Xi,x}{t}}{\jwpatpho{\Gamma;\Delta;\Xi}{\tabsU{x}{t}}}

  \rrulepp{}{\jwpatpho{\Gamma;\Delta;\Xi}{t}}{\jwpatpho{\Gamma;\Delta;\Xi}{u}}{\jwpatpho{\Gamma;\Delta;\Xi}{\tapp{t}{u}}}

  \rrulepp{}{F \in \Delta}{\forall x,y \in l, x \neq y \land x \in \Xi \land y \in \Xi}{\jwpatpho{\Gamma;\Delta;\Xi}{\tapp{F}{l}}}
\end{trules}

\begin{trules}{Rules}{coucouagain}
  \rrulep{}{\forall \sigma : \Delta \to \mathcal{T}, \jct{\Gamma}{l\sigma}{A} \Rightarrow \jct{\Gamma}{r\sigma}{A} }{\jwtr{\Gamma}{l \mrw{\Delta} r}}
  
  \rruleppp{}{\jwpat{\Gamma;\Delta}{l}}{FV(r) \subseteq FV(l) = \Delta}{\jwtr{\Gamma}{l \mrw{\Delta} r}}{\jwr{\Gamma}{l \mrw{\Delta} r}}
\end{trules}

\begin{trules}{Typing system}{oopsi}
  \rrule{}{\jcw{\emptyset}}

  \rrulepp{}{\jcw{\Gamma}}{\jct{\Gamma}{A}{s}}{\jcw{\Gamma,x : A}}

  \rruleppp{}{\jcw{\Gamma}}{\jwr{\Gamma}{l \mrw{\Delta} r}}{\beta\Gamma \text{ is terminating and confluent}}{\jcw{\Gamma, l \mrw{\Delta} r}}  

  \rrulep{}{\jcw{\Gamma}}{\jct{\Gamma}{\Type}{\Kind}}
  
  \rrulepp{}{\jcw{\Gamma}}{x \in \Gamma}{\jct{\Gamma}{x}{A}}

  \rrulepp{}{\jct{\Gamma}{A}{\Type}}{\jct{\Gamma,x:A}{B}{s}}{\jct{\Gamma}{\tpi{x}{A}{B}}{s}}
  
  \rrulepp{}{\jct{\Gamma,x:A}{t}{B}}{\jct{\Gamma}{\tpi{x}{A}{B}}{s}}{\jct{\Gamma}{\tabs{x}{A}{t}}{\tpi{x}{A}{B}}}

  \rrulepp{}{\jct{\Gamma}{t}{\tpi{x}{A}{B}}}{\jct{\Gamma}{u}{A}}{\jct{\Gamma}{\tapp{t}{u}}{\msubst{B}{x}{A}}}

  \rruleppp{}{\jct{\Gamma}{t}{A}}{\jct{\Gamma}{B}{s}}{A \meq{\beta\Gamma} B}{\jct{\Gamma}{t}{B}}
\end{trules}