<commit_before>\documentclass[preprint, authoryear]{sigplanconf}

\usepackage{amsmath}
\usepackage{verbatim}

%% Structure
\newenvironment{structure}{\footnotesize\verbatim}{\endverbatim}
%\newenvironment{structure}{\comment}{\endcomment}


\begin{document}

%\conferenceinfo{WXYZ '05}{date, City.} 
%\copyrightyear{2005} 
%\copyrightdata{[to be supplied]} 

%\titlebanner{banner above paper title}        % These are ignored unless
%\preprintfooter{short description of paper}   % 'preprint' option specified.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Title
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\title{Generic programming is just programming}
% Or something mentionning levitation. Feel free to change. 
% \subtitle{Subtitle Text, if any}


%% Alphabetical ordering.
\authorinfo{<NAME>}
           {Institute of Cybernetics, Tallinn University of Technology}
           {<EMAIL>}
\authorinfo{Pierre-\'{<NAME> \\ <NAME>}
           {University of Strathclyde}
           {\{<EMAIL>,<EMAIL>}
\authorinfo{<NAME>}
           {University of Nottingham}
           {<EMAIL>}


\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Abstract
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{abstract}
This is the text of the abstract.
\end{abstract}

%\category{CR-number}{subcategory}{third-level}

%\terms
%term1, term2

%\keywords
%keyword1, keyword2

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Introduction
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}

The text of the paper begins here. \cite{morris:spf}

ACM bullet points, we offer:
\begin{itemize}
\item a closed presentation of data-types (no generativity requires)
  subsuming standard inductive families (some popular extensions
  excluded for now)
\item descriptions of data-types are first-class (indeed,
  self-encoded)
\item ``generic programming is just programming''
\item first serious attempt to design a language for generic
  programming, except possibly Lisp
\end{itemize}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Desc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{A simple universe of descriptions}

\begin{structure}
<- a universe of simple inductive types
    -> nil, arg, ind, hind
<- levitation
\end{structure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% IDesc<commit_msg>Desc@ICFP: I remembered the plan for type theory description<commit_after>\documentclass[preprint, authoryear]{sigplanconf}

\usepackage{amsmath}
\usepackage{verbatim}

%% Structure
\newenvironment{structure}{\footnotesize\verbatim}{\endverbatim}
%\newenvironment{structure}{\comment}{\endcomment}


\begin{document}

%\conferenceinfo{WXYZ '05}{date, City.} 
%\copyrightyear{2005} 
%\copyrightdata{[to be supplied]} 

%\titlebanner{banner above paper title}        % These are ignored unless
%\preprintfooter{short description of paper}   % 'preprint' option specified.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Title
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\title{Generic programming is just programming}
% Or something mentionning levitation. Feel free to change. 
% \subtitle{Subtitle Text, if any}


%% Alphabetical ordering.
\authorinfo{<NAME>}
           {Institute of Cybernetics, Tallinn University of Technology}
           {<EMAIL>}
\authorinfo{Pierre-\'{E}<NAME> \\ <NAME>}
           {University of Strathclyde}
           {\{<EMAIL>,<EMAIL>}
\authorinfo{<NAME>}
           {University of Nottingham}
           {<EMAIL>}


\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Abstract
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{abstract}
This is the text of the abstract.
\end{abstract}

%\category{CR-number}{subcategory}{third-level}

%\terms
%term1, term2

%\keywords
%keyword1, keyword2

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Introduction
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}

The text of the paper begins here. \cite{morris:spf}

ACM bullet points, we offer:
\begin{itemize}
\item a closed presentation of data-types (no generativity requires)
  subsuming standard inductive families (some popular extensions
  excluded for now)
\item descriptions of data-types are first-class (indeed,
  self-encoded)
\item ``generic programming is just programming''
\item first serious attempt to design a language for generic
  programming, except possibly Lisp
\end{itemize}

\begin{structure}
<- presentation of the Core theory
    -> judgemental equality (extensional (a la OTT?))
    /> not Epigram specific 
        <- having OTT just buys you more stuffs
\end{structure}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Desc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{A simple universe of descriptions}

\begin{structure}
<- a universe of simple inductive types
    -> nil, arg, ind, hind
<- levitation
\end{structure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% IDesc
{'fraction_non_alphanumeric': 0.30792624976240257, 'fraction_numerical': 0.0038015586390420073, 'mean_word_length': 5.472324723247232, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2467112', 'n_tokens_mistral': 1457, 'n_tokens_neox': 1291, 'n_words': 374}