[Git][monnier/typer][report/itd] -
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... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/67b389106e3be35e180f38b1afa4804c7a51... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan