1\section{The Core Type Theory}
3\label{sect:typechecking}
5High level \Idris{} programs, as described in Section \ref{sect:hll}, are
6\remph{elaborated} to a small core language, \TT{}, then type checked.
7\TT{} is a dependently typed $\lambda$-calculus with inductive families
8and pattern matching definitions similar to UTT~\cite{luo1994}, and building
9on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
11core language as small as is reasonably possible, which has several advantages: it is
12easy to type check, since type checking dependent type theory is well understood
13~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping
14the core language small increases our confidence that these important components of
15the language are correct. In this section, we describe \TT{} and
18\subsection{\TT{} syntax}
20The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:
23\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.
24\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.
25\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the
26type of types, and may be extended with other primitives.
29We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$,
30or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with
31the high level language. Universe levels on sets ($\Type_i$) may be left implicit and
32inferred by the machine~\cite{pollack1990implicit}.
35\begin{array}{rll@{\hg}rll}
36\vt ::= & \vc & (\mbox{constant}) &
37\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\
39 \mid & \vx & (\mbox{variable}) &
40 \mid & \LET\:\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\
42 \mid & \vb\SC\:\vt & (\mbox{binding}) &
43 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\
45 \mid & \vt\:\vt & (\mbox{application}) &
46% \mid & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\
48% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\
50 \vc ::= & \Type_i & (\mbox{type universes}) \\
51 \mid & \vi & (\mbox{integer literal}) \\
52 \mid & \VV{str} & (\mbox{string literal}) \\
55{\TT{} expression syntax}
58A \TT{} program is a collection of \demph{inductive family} definitions (Section
59\ref{sect:inductivefams}) and \demph{pattern matching} function definitions (Section
60\ref{sect:patdefs}), as well as primitive operators on constants.
61Before defining these, let us define the semantics of \TT{}
64\subsection{\TT{} semantics}
66The static and dynamic semantics of \TT{} are defined mutually, since
67evaluation relies on a well-typed term, and type checking relies on
68evaluation. Everything is defined relative
69to a context, $\Gamma$. The empty context
70is valid, as is a context extended with a $\lambda$, $\forall$ or
74\Axiom{\proves\RW{valid}}
76\Rule{\Gamma\proves\RW{valid}}
77{\Gamma;\vb\proves\RW{valid}}
80\subsubsection{Evaluation}
82\label{sect:evaluation}
84Evaluation of \TT{} is defined by contraction schemes, given in Figure
85\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
86by one of the following schemes:
89\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
90the bound variable. We define $\beta$-contraction simply by replacing the $\lambda$-binding
92\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
96We use the following contextual closure rule to reduce a $\LET$ binding by creating
97a $\delta$-reducible expression:
100\Rule{\Gamma;\LET\:\vx\defq\vs\proves\vt\leadsto\vu}
101{\Gamma\proves\LET\:\vx\defq\vs\Hab\vS\SC\vt\leadsto\vu}
104\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
105is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
106is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
107then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
108contractions and reversed contractions. Terms which are convertible are also said to
109be definitionally equal.
110The evaluator can also be extended by defining pattern matching functions, which
111will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
112matching functions can be understood as extending the core language with high level
117\beta\mathrm{-contraction} &
119\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\:\vs\leadsto\LET\:\vx\defq\vs\Hab\vS\SC\vt
121\delta\mathrm{-contraction} &
123\Gamma;\LET\:\vx\defq\vs\Hab\vS;\Gamma'
129{\TT{} contraction schemes}
134\subsubsection{Typing rules}
136\label{sect:typerules}
138The type inference rules for \TT{} expressions are given in Figure \ref{typerules}.
139These rules use the \demph{cumulativity} relation, defined in
140Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe level,
141to prevent Girard's paradox~\cite{coquand1986analysis}. Cumulativity allows programs at
142lower universe levels to inhabit higher universe levels. In practice, universe levels
143can be left implicit (and will be left implicit in the rest of this paper) ---
144the type checker generates a graph of constraints between universe levels (such
145as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
146are no cycles. Otherwise, the typing rules are standard and type inference can
147be implemented in the usual way~\cite{loh2010tutorial}.
149\FFIG{\begin{array}{c}
151\Rule{\Gamma\proves\RW{valid}}
152{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
155\Rule{\Gamma\proves\RW{valid}}
156{\Gamma\vdash\vi\Hab\TC{Int}}
159\Rule{\Gamma\proves\RW{valid}}
160{\Gamma\vdash\VV{str}\Hab\TC{String}}
163\Rule{\Gamma\proves\RW{valid}}
164{\Gamma\vdash\TC{Int}\Hab\Type_0}
167\Rule{\Gamma\proves\RW{valid}}
168{\Gamma\vdash\TC{String}\Hab\Type_0}
171%\Rule{(\pat{\vx}{\vS})\in\Gamma}
172%{\Gamma\vdash\vx\Hab\vS}
175%\Rule{(\pty{\vx}{\vS})\in\Gamma}
176%{\Gamma\vdash\vx\Hab\vS}
179\Rule{(\lam{\vx}{\vS})\in\Gamma}
180{\Gamma\vdash\vx\Hab\vS}
183\Rule{(\all{\vx}{\vS})\in\Gamma}
184{\Gamma\vdash\vx\Hab\vS}
187\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
188{\Gamma\vdash\vx\Hab\vS}
191\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
192{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
195\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}
196{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}
199\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}
200{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}
201\:(\exists\vp.\vm\le\vp,\:\vn\le\vp)
204\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg
205 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\
206 \Gamma\proves\vS\Hab\Type_n\hg
207 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}
209{\Gamma\vdash\LET\:\vx\defq\ve_1\Hab\vS\SC\:\ve_2\Hab
211%\Let\:\vx\Hab\vS\defq\ve_1\:\IN\:\vT}
215\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg
216 \Gamma\proves\vA\cumul\vA'}
217 {\Gamma\proves\vx\Hab\vA'}
220{Typing rules for \TT{}}
225\Rule{\Gamma\proves\vS\converts\vT}
226{\Gamma\proves\vS\cumul\vT}
228\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
230\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
231{\Gamma\proves\vR\cumul\vT}
233\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
234{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
240\subsection{Inductive Families}
242\label{sect:inductivefams}
244Inductive families \cite{dybjer1994inductive} are a form of simultaneously
245defined collection of algebraic data types which can be parameterised over
246\remph{values} as well as types. An inductive family is declared
247in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
249follows, using vector notation, $\tx$, to indicate a
250sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
254\Data\hg\TC{T}\:(\tx\Hab\ttt)\Hab\vt\hg\Where\hg
255\DC{c}_1\Hab\vt\:\mid\:\ldots\:\mid\:\DC{c}_n\Hab\vt
259Constructors may take recursive arguments in the family
260$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---
261if such indices do not involve $\TC{T}$ then the constructor is
262\demph{strictly positive}, which ensures that recursive arguments of the
263constructor are structurally smaller than the value itself.
265For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
268\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\:\mid\:\suc\Hab\fbind{\vk}{\Nat}{\Nat}
271A data type may have zero or more parameters (which are invariant
272across a structure) and a number of indices, given by the type. For
273example, the \TT{} equivalent of \tTC{List} is parameterised over its element type:
277\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where
279& \nil\Hab\List\:\va\\
280\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\:\va}{\List\:\va}}
286parameterised over values. Using this, we can declare the type of
287vectors (lists with length), where the empty list is statically known
288to have length zero, and the non empty list is statically known to
289have a non zero length. The \TT{} equivalent of \tTC{Vect} is parameterised over its element type,
290like $\List$, but \remph{indexed} over its length. Note also that the length
291index $\vk$ is given \remph{explicitly}.
295\Data\hg\Vect\:(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\
297& \nil\Hab\Vect\:\va\:\Z\\
298\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
299\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\:\va\:\vk}{\Vect\:\va\:(\suc\:\vk)}}
305\subsection{Pattern matching definitions}
309\subsubsection{Syntax}
311A pattern matching definition for a function named $\FN{f}$ takes the following form,
312consisting of a type declaration followed by one or more pattern clauses:
317\pat{\tx_1}{\ttt_1}\SC\FN{f}\:\ttt_1\:=\:\vt_1\\
319\pat{\tx_n}{\ttt_n}\SC\FN{f}\:\ttt_n\:=\:\vt_n\\
323A pattern clause consists of a list of pattern variable bindings,
324and a left and right hand side, both of which
325are \TT{} expressions. Each side is type checked relative to the variable bindings,
326and the types of each side must be convertible. Additionally, the
327left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
328and the number of arguments must be the same in each clause. The right hand
329sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
330be recursive. Termination analysis is implemented separately. The validity of a pattern
331clause is defined by the following rule:
335\Gamma;\lam{\tx}{\tU}\proves\FN{f}\:\tts\Hab\vS\hg
336\Gamma;\lam{\tx}{\tU}\proves\ve\Hab\vT\hg
337\Gamma\proves\vS\converts\vT}
339\Gamma\proves\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve\:\RW{valid}
343A valid pattern matching definition effectively extends \TT{} with a new constant,
344with the given type (extending the initial typing rules given in Section \ref{sect:typerules})
345and reduction behaviour (extending the initial reduction rules given in Section
346\ref{sect:evaluation}).
348\subsubsection{Semantics}
350Matching on an expression proceeds by comparing the expression to
351each match clause in order, resulting in either:
354\item \demph{Success}, with pattern variables mapping to expressions
355\item \demph{Failure}, with matching continuing by proceeding to the next match clause
356\item Matching being \demph{blocked}, for example by attempting to match a variable
357against a constructor pattern. In this case, no reduction occurs, because instantiating
358the variable may provide enough information for the clause to match.
361% Pat(x args) => x (Pat' args)
365In order to implement pattern matching, we must separate the \remph{accessible} and
366\remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible
367to match against it) if it is constructor headed, or a variable. Inaccessible patterns
368are converted to ``match anything'' patterns. We convert clauses to matchable pattern
369clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
370We extend the vector notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
371$\MO{Pat}$ operation across a list of arguments.
376& \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve)
377 & \MoRet{\FN{f}\:(\vec{\MO{Pat}}\:\tts)\:=\:\ve}
381& \MO{Pat} & (\vx\:\tts) & \MoRet{\vx\:(\vec{\MO{Pat}}\:\tts)
382 \hg\mbox{(if $\MO{Con}\:\vx$ and $\MO{Arity}\:\vx = \MO{Length}\:\tts$)}} \\
383& \MO{Pat} & \vx & \MoRet{\vx} \hg\mbox(if $\vx$ is a pattern variable)\\
384& \MO{Pat} & \cdot & \MoRet{\_} \hg\mbox(in all other cases)\\
388{Building matchable pattern clauses}
392% Match (c args, c args') => Match' (args, args')
393% Match (c args, x) => Blocked
394% Match (x, t) => Success (x => t)
395% Match (_, t) => Success ()
397\newcommand{\Blocked}{\mathsf{Blocked}}
398\newcommand{\Success}{\mathsf{Success}}
399\newcommand{\Failure}{\mathsf{Failure}}
401Pattern matching is invoked by the evaluator on encountering a function with
402a pattern matching definition applied to some arguments. If successful, pattern
403matching returns a new expression, which can then be reduced further.
404Figure \ref{pmatch} gives the semantics of pattern matching a collection of
406$\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
407turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
408matching terminates. If matching a clause returns $\Failure$, then matching proceeds
409with the next clause. The algorithm uses the following meta-operations:
412\item $\MO{Con}\:\vx$, which returns true if $\vx$ is a constructor name
413\item $\MO{Arity}\:\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
415\item $\MO{Length}\:\tts$, which returns the length of the telescope $\tts$
422& \MO{MatchArg} & (\vx\:\tts) & (\vx\:\tts')
423 & \MoRet{\vec{\MO{MatchArg}}\:\tts\:\tts'\hg\mbox{(if $\MO{Con}\:\vx$)}}\\
424& \MO{MatchArg} & (\vx\:\tts) & \vx & \MoRet{\Blocked} \\
425& \MO{MatchArg} & \vx & \vt & \MoRet{\Success\:(\vx\mapsto\vt)} \\
426& \MO{MatchArg} & \_ & \vt & \MoRet{\Success\:()} \\
427& \MO{MatchArg} & \cdot & \cdot & \MoRet{\Failure}
431& \MO{MatchClause} & (\vf\:\tp = \ve) & (\vf\:\tts) &
434 \Success\:\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Success\:(\tx,\tv)$)}\\
435 \Blocked\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Blocked$)}\\
436 \Failure\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Failure$)}\\
439& \MO{MatchClause} & (\vf\:\tp = \ve) & \cdot & \MoRet{\Failure} \\
443& \MO{Match} & (\vc ; \tc) & \ve &
446 \Success\:\vx\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Success\:\vx)$} \\
447 \Blocked\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Blocked)$} \\
448 \MO{Match}\:\tc\:\ve\hg\mbox{(otherwise)}
451& \MO{Match} & \cdot & \ve & \MoRet{\Failure}
455{Pattern matching semantics}
458By convention, we write the application of a meta-operation $\MO{Op}$
459to a telescope $\tx$ as $\vec{\MO{Op}}\:\tx$.
460In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
461a tree of case expressions~\cite{Augustsson1985}.
463\subsection{Totality checking}
465In order to ensure termination of type checking, and therefore its decidability,
466we must distinguish terms for which evaluation definitely terminates, and
467those which may diverge. \TT{} takes a simple but pragmatic and
468effective approach to termination
469checking: any functions which do not satisfy a syntactic constraint on recursive
470calls are marked as \emph{partial}. Additionally, any function which calls a partial
471function are uses a data type which is not strictly positive is also marked as
472partial. The syntactic constraint we use is that a recursive call in a pattern
473clause must have an argument which is structurally smaller than an input argument
474in the same position. \TT{} also marks functions which do not cover all possible
475inputs as partial. This totality checking is independent of the rest of the type
476theory, and can be extended in future.
478This approach, separating the termination requirement from the type theory, means that
479an \Idris{} programmer makes the decision about the importance of totality for each
480function rather than having the totality requirement imposed by the type theory.
482\subsection{From \Idris{} to \TT{}}
484\TT{} is a very small language, consisting only of data declarations and pattern matching
485function definitions. There is no significant innovation in the design of \TT{}, and this
486is a deliberate choice --- it is a combination of small, well-understood components.
487The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
488pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
489in the correctness of the kernel of \TT{}, and any higher level language feature
490can be translated into \TT{}, we can be more confident of the correctness of the high
491level language implementation than if it were implemented directly.
493The process of elaborating a high level language into a core type theory like \TT{} is,
494however, less well understood, and presents several challenges depending on the
495features of the high level language.
496%Elaboration has been implemented in various different ways,
497%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
499\subsubsection{Example Elaboration}
501Consider the following \Idris{} function:
503\begin{SaveVerbatim}{vadd}
505vAdd : Num a => Vect a n -> Vect a n -> Vect a n
507vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys
513This adds corresponding elements of vectors of the same length. The vectors can contain
514any numeric type, overloaded using the \texttt{Num} type class. In order to elaborate
515this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
517The first step is to make the implicit arguments explicit, using a placeholder
518to stand for the arguments we have not yet resolved. The type class argument is
519also treated as an implicit argument, to which we give the name \texttt{c}:
521\begin{SaveVerbatim}{vAddImp}
523vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n
524vAdd _ _ c (Nil _) (Nil _) = (Nil _)
525vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
526 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
531Next, we resolve the implicit arguments. Each implicit argument can only take
532one value for this program to be type correct --- these are solved by a unification
535\begin{SaveVerbatim}{vAddImpSolve}
537vAdd : (a : Set) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n
538vAdd a O c (Nil a) (Nil a) = Nil a
539vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
540 = (::) a k ((+) c x y) (vAdd a k c xs ys)
543\useverb{vAddImpSolve}
545Finally, to build the \TT{} definition, we need to find the type of each pattern variable
546and state it explicitly. This leads to the \TT{} definition in Figure \ref{ttvadd},
547switching to \TT{} notation from the ASCII \Idris{} syntax.
552\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to
553 \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\
556\begin{array}{lccccccc}
558\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\
559\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\
562\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
563\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;
564\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk
568\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc
569 & ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
570 & ((\DC{::})\;\va\;\vk\;\vy\;\vys)
572 & & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}
576{Pairwise addition of vectors in \TT{}}
579\subsubsection{An observation}
581\Idris{} programs may contain several high level constructs not present in \TT{}, such
582as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
583and \texttt{case} constructs. We would like the high level language to be as expressive
584as possible, while remaining possible to translate to \TT{}.
586Before considering how to achieve this, we make an observation about the distinction between
587programming and theorem proving with dependent types, and appropriate mechanisms for
588constructing programs and theorems:
591\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,
592in that it allows a programmer to express exactly the computational behaviour of a function.
593\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},
594are a convenient abstraction for building proofs and programs by \remph{refinement}.
597The idea behind the \Idris{} elaborator, therefore, is to use the high level program
598to direct \demph{tactics} to build \TT{} programs by refinement. We implement the
599elaborator as an Embedded Domain Specific Language (EDSL) in Haskell.
601of this paper, we describe the EDSL, and demonstrate how it can be used to implement
602all of the high level features of \Idris{}.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list