Stefan pushed to branch report/itd at Stefan / Typer
Commits: 67b38910 by Stefan Monnier at 2018-10-06T01:03:20Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -166,7 +166,7 @@ \section{Introduction}
Typer is a language in the tradition of Coq, Lean, and Agda, but focusing on -programs more than proofs, like Idris, F-star, and ATS. +programs more than proofs, like Idris, F-star~\cite{Swamy16}, and ATS.
Typer needs a good target language: \begin{itemize} @@ -647,7 +647,6 @@ types, to make sure we can apply \kw{case} to them. \end{displaymath}
\begin{mathpar} - %% FIXME: Define pos (will require something like `con`) \Infer{\Jtyper{\tau}{s} \ \Jtyper[\Gamma,x:\tau]{e}{\tau} \ \Jpos[{x}]e}
View it on GitLab: https://gitlab.com/monnier/typer/commit/67b389106e3be35e180f38b1afa4804c7a51...