From 18848ceaae0e036618eba77ef63d30cb02ac1563 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 20 Apr 2023 16:52:56 -0400
Subject: [PATCH] syntax discussed in today's meeting
---
notes/intensional-syntax.tex | 68 ++++++++++++++++++++++++++++++++++++
1 file changed, 68 insertions(+)
create mode 100644 notes/intensional-syntax.tex
diff --git a/notes/intensional-syntax.tex b/notes/intensional-syntax.tex
new file mode 100644
index 0000000..ed4d9c8
--- /dev/null
+++ b/notes/intensional-syntax.tex
@@ -0,0 +1,68 @@
+\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}
--
GitLab