intensional-syntax.tex 1.52 KiB
\documentclass{article}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{tikz-cd}
\usepackage{mathpartir}
\usepackage{stmaryrd}
\usepackage{parskip}
\usepackage{tikz-cd}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{nonnum-theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]
\newcommand{\later}{{\vartriangleright\hspace{-2px}}}
\newcommand{\nxt}{\texttt{next}}
\newcommand{\calS}{\mathcal{S}}
\newcommand{\gfix}{\texttt{gfix}}
\newcommand{\calU}{\mathcal{U}}
\newcommand{\laterhat}{\widehat{\later}}
\newcommand{\El}{\mathsf{El}}
\newcommand{\lift}{L_\mho}
\newcommand{\lifthat}{\widehat{L_\mho}}
\newcommand{\To}{\Rightarrow}
\newcommand{\calC}{\mathcal{C}}
\newcommand{\Set}{\texttt{Set}}
\newcommand{\Yo}{\mathsf{Yo}}
\newcommand{\Hom}{\mathsf{Hom}}
\newcommand{\inl}{\texttt{inl}}
\newcommand{\inr}{\texttt{inr}}
\newcommand{\alt}{\,|\,}
\begin{document}
\title{Intensional Syntax}
\author{Max S. New and Eric Giovannini}
\maketitle
\begin{mathpar}
\begin{array}{rcl}
\textrm{Value Types} & ::= & \mathbb N \alt D \alt A \rightharpoonup A'\alt \later A\\
\textrm{Comp Types} & ::= & \mathcal L A
\end{array}
\end{mathpar}
What are the rules for $\later$?
\begin{mathpar}
\inferrule
{\Gamma \vdash V : A}
{\Gamma \vdash \nxt\, V : \later A}
\inferrule
{}
{\Gamma \vdash \theta : \later A \rightharpoonup A}
\theta(\nxt x) = \theta(y); \texttt{ret}\, x
\end{mathpar}
\end{document}