\chapter{Monads}
\label{chap:monads}

Pure functional programming can sometimes feel overly restrictive.
\emph{Effectful functional programming} provides idioms that alleviate some of
these restrictions, giving us the impression of programming with side effects,
exceptions, nondeterminism, and other effects.

The underlying abstraction is called \emph{monad}. Monads generalize programs
with side effects. They are popular in Haskell to write imperative programs. In
Lean, they are used to express imperative programs and to reason about them.
They are even useful for programming Lean itself, as we will see in
Chapter~\ref{chap:metaprogramming}.

These notes are inspired by Chapter 7 of \emph{Programming in Lean}
\cite{programming-in-lean}. We also refer to Chapter~14 of \emph{Real World
Haskell} \cite{osullivan-et-al-2008} for a general introduction to effectful
functional programming.

\section{Introductory Example}
\label{sec:introductory-example}

Consider the following programming task:
%
\begin{quote}
Implement a function
\li{sum_2_5_7 ns} that sums up the second, fifth, and seventh items of a list
\li{ns} of natural numbers. Use \li{option ℕ} for the result so that if the list
has too few items, return \li{option.none}.
\end{quote}
%
A straightforward solution would be as follows:

\lstinputlisting[linerange=sum_2_5_7-q]{../lean/love06_monads_demo_master.lean}
%
(Confusingly, \li{list.nth} counts elements from 0.) The code is quite
inelegant, because of all the pattern matching on \li{option}. Although the
programming task is contrived, we can all recall writing code with nested error
handling and ever increasing indentation levels.

We can do better, by concentrating all the ugliness in one function:

\lstinputlisting[linerange=connect-q]{../lean/love06_monads_demo_master.lean}
%
The \li{connect} function operates on an option---a value of type \li{option α}.
If the value is \li{option.none}, we leave it as is. This corresponds to an error
condition, and errors are remembered. Otherwise, the value is of the form
\li{option.some a}, and we apply the operation \li{f} on \li{a}---or
\emph{bind} \li{f}'s argument to \li{a}. We can now use \li{connect} to
program our sum function:

\lstinputlisting[linerange=sum_2_5_7₂-q]{../lean/love06_monads_demo_master.lean}
%
Intuitively, the program performs the following steps:
%
\begin{itemize}
\item[1.] Extract the second item from the list. If it is \li{option.none}, we are
  done. Otherwise, bind \li{n2} to this item and continue with the next step.
\item[2.] Perform the same for the fifth and seventh item, mutatis mutandis.
\item[3.] Return the sum of \li{n2}, \li{n5}, and \li{n7} in an
  \li{option.some} wrapper.
\end{itemize}
%
Semantically, our new function \li{sum_2_5_7₂} is equal to the original
\li{sum_2_5_7}.

Instead of defining \li{connect} ourselves, we could have used Lean's
predefined general \li{bind} operation. It takes the same arguments in the same
order. Here is the new code:

\lstinputlisting[linerange=sum_2_5_7₃-q]{../lean/love06_monads_demo_master.lean}
%
We also use the predefined \li{pure} function instead of \li{option.some} to
convert a pure \li{α} value to an option.

One of the advantages of using the predefined notions is that they provide
syntactic sugar, in the form of the \li{>>=} operator:

\lstinputlisting[linerange=sum_2_5_7₄-q]{../lean/love06_monads_demo_master.lean}
%
The syntax \li{ma >>= f} expands to \li{bind ma f}, where \li{ma} stands for
``maybe an \li{α}.''

The penultimate version of the sum program uses heavier syntactic sugar:

\lstinputlisting[linerange=sum_2_5_7₅-q]{../lean/love06_monads_demo_master.lean}
%
The \li{do} notation provides a convenient syntax for effectful programs. The
program \hbox{\li{do a ← ma, t}} is equivalent to \li{ma >>= (λa, t)}. If we are
not interested in the result of \li{ma}'s computation, we can omit the
\li{a ←} binding and write \li{do ma, t}, which expands to
\li{ma >>=} \li{(λ_, t)}.

The \li{do} notation conveniently allows multiple \li{←} bindings in a
single block. This brings us to the final version of the program:

\lstinputlisting[linerange=sum_2_5_7₆-q]{../lean/love06_monads_demo_master.lean}
%
Each line with an arrow \li{←} attempts to read a value. In case of failure, the
entire program evaluates to \li{option.none}.

The above function can be read as an imperative program where each of the
\li{list.nth} calls can throw an exception. But even though the notation has an
imperative flavor, the function is a pure functional program.

\section{Two Operations and Three Laws}
\label{sec:two-operations-and-three-laws}

The \li{option} type constructor is an example of a monad, called the
\emph{option monad}. In general, a monad is a unary type constructor
\li{m : Type → Type} that depends on some type parameter \li{α} equipped with
two distinguished operations:
%
\begin{center}
\begin{tabular}{@{}r@{}c@{}l@{}}
\lic|pure {α : Type}| & ${}:{}$ & \lic|α → m α| \\
\lic|bind {α β : Type}| & ${}:{}$ & \lic|m α → (α → m β) → m β| \\
\end{tabular}
\end{center}
%
As usual, curly braces denote implicit arguments. For options, the \li{pure}
operation is simply \li{option.some}, whereas \li{bind} is what we called
\li{connect}.

Recall that a value of type \li{m α} is an effectful program. The \li{pure}
operation embeds a pure, effectless program of type \li{α} in \li{m α}. The
\li{bind} operation composes two effectful programs, of types \li{m α} and
\li{m β}. The first program's output, of type \li{α}, is passed to the second
program. The second program's output is also the output of the composite
program.

We can think of a monad as a box containing some data. The box captures some
special effect (e.g., exceptions, a mutable state). The \li{pure} operation
puts data into the box, whereas \li{bind} allows us to access the data in the
box and modify it---possibly even changing its type, since the result has type
\li{m β}, not \li{m α}. There is, however, no general way to extract the data
from the box---i.e., to obtain an \li{α} from an \li{m α}. There might not be
any \li{α} value in it, or there might be several.

To summarize, \li{pure a} is a box containing the value \li{a}, with
no side effects, whereas \li{bind ma f} (also written \li{ma >>=} \li{f} or
\li{do a ← ma, f a}) executes \li{ma}, then executes \li{f} with the boxed
result \li{a} of \li{ma}. It is convenient to use names such as \li{ma} or
\li{mb} for monad values of type \li{m α} or \li{m β}, and \li{a} or \li{b} for
data of type \li{α} or \li{β}.

Monads are an abstract concept with many applications. The option monad is only
one instance among many. The following table gives an overview of some monad
instances and their effects.

\vskip4\smallskipamount

\centerline{\tabletsmall\begin{tabular}{@{}l@{\quad}l@{}}
\toprule
Type & Effect \\
\midrule
\li|id α|       & no effect \\
\li|option α|   & simple exceptions \\
\li|\σ → α × σ| & threading through a state of type \li|\σ| \\
\li|set α|      & nondeterministic computations returning \li|\α| values \\
\li|t → α|      & reading elements of type \li|t| (e.g., a configuration) \\
\li|\ℕ × α|     & adjoining running time (e.g., to model algorithmic complexity) \\
\li|string × α| & adjoining text output (e.g., for logging) \\
\li|prob α|     & probability (e.g., using random number generators) \\
\li|io α|       & interaction with the operating system \\
\li|tactic α|   & interaction with the proof assistant \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

All of the above are unary type constructors \li{m} with an argument \li{α}.
Some effects can be combined (e.g., \li{option (t → α)}). Some effects are not
executable (e.g., \li{prob α}); they are nonetheless useful for modeling
programs abstractly in the logic. Specific type constructors \li{m} may provide
further operators beyond \hbox{\li{pure}} and \li{bind}. For example, they may
provide a way to extract the boxed value.

Monads have several benefits. They provide the highly readable \li{do}
notation. They support generic operations, such as \li|list.|\hbox{\li|mmap {α β :|}
\hbox{\li|Type} : (α → m β) →|} \hbox{\li|list α → m (list β)|,} that work
uniformly for all monads~\li{m}. To quote \emph{Programming in Lean}
\cite{programming-in-lean}:
%
\begin{quote}
The power of the abstraction is not only that it provides general functions
and notation %the
that can be used in all these various instantiations, but also
that it provides a helpful way of thinking about what they all have in
common.
%
\end{quote}
%
Besides being a useful computer science concept, monads provide a nice example
of axiomatic reasoning, the axioms being the monad laws, introduced below.

\newcommand\BIGEQ{\qquad\smash{\lower.2ex\hbox{\Large\li|=|}}\qquad\hbox{}}

The \li{bind} and \li{pure} operations are normally required to obey three
laws. The \li{bind} operation combines two programs. If either of these is a
pure program, we can inline it and eliminate the \li{bind}. This gives us the
first two laws:

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}p{7.5em}@{}l@{}p{7.5em}@{}}
\lic|do| \\
\quad \lic|a' ← pure a,|\! & \BIGEQ & \lic|f a| \\
\quad \lic|f a'|
\end{tabular}}

\vskip\abovedisplayshortskip

\noindent
and

\vskip\abovedisplayshortskip

\centerline{\begin{tabular}{@{}p{7.5em}@{}l@{}p{7.5em}@{}}
\lic|do| \\
\quad \lic|a ← ma,| & \BIGEQ & \lic|ma| \\
\quad \lic|pure a|
\end{tabular}}

\vskip\belowdisplayskip

\noindent
The third law is an associativity rule for bind. It allows us to flatten a
nested computation:

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}p{7.5em}@{}l@{}p{7.5em}@{}}
\lic|do| &
  & \lic|do| \\
\quad \lic|b ← do|~\texttt{\char`\{} &
  & \quad \lic|a ← ma,| \\
\qquad \lic|a ← ma,| & \BIGEQ
  & \quad \lic|b ← f a,| \\
\qquad \lic|f a|~\texttt{\char`\}}\lic|,| &
  & \quad \lic|g b| \\
\quad \lic|g b|
\end{tabular}}

\vskip\belowdisplayskip

\noindent
Notice that we can use curly braces \li|{ }| around the body of a \li{do} block
to delimit it, instead of enclosing the entire block in parentheses \li|( )|.

The \li{do} notation is compatible with \li{let}. Instead of

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}l@{}}
\lic|do| \\
\quad \lic|a' ← pure a,| \\
\quad \lic|b ← f a',| \\
\quad \lic|g b| \\
\end{tabular}}

\vskip\belowdisplayskip

\noindent
we can write

\vskip\abovedisplayshortskip

\centerline{\begin{tabular}{@{}l@{}}
\lic|do| \\
\quad \lic|let a' := a in| \\
\qquad \lic|do| \\
\qquad\quad \lic|b ← f a',| \\
\qquad\quad \lic|g b| \\
\end{tabular}}

\vskip\belowdisplayskip

\noindent
or

\vskip\abovedisplayskip

\centerline{\begin{tabular}{@{}l@{}}
\lic|do| \\
\quad \lic|let a' := a,| \\
\quad \lic|b ← f a',| \\
\quad \lic|g b| \\
\end{tabular}}

\vskip\belowdisplayskip

\section{A Type Class}
\label{sec:a-type-class}

Monads are a mathematical structure, so we use a type class to specify them in
Lean. Recall that a type class is a structure type that is parameterized,
typically by a type, but here by a type constructor \li{m : Type → Type}.
Whenever we use a field from the type class on a concrete~\li{m}, the type
class inference mechanism retrieves the relevant structure value---the type
class instance.

A possible Lean definition of monads, together with the three laws, follows:

\lstinputlisting[linerange=lawful_monad-q]{../lean/love06_monads_demo_master.lean}

Let us study this definition step by step:

\begin{itemize}
\item We are creating a structure parameterized by a unary type
  constructor~\li{m}.

\item The structure inherits the fields, and any syntactic sugar, from
  structures called \li{has_bind} and \li{has_pure}. These provide the
  \li{bind} and \li{pure} operations on \li{m}, with the expected types and
  the syntactic sugar.

\item Finally, three fields (\li{pure_bind}, \hbox{\li{bind_pure},}
  and \li{bind_assoc}) are added to those already provided by
  \li{has_}\allowbreak\li{bind} and \hbox{\li{has_pure}.} Each field is a proof
  of one of the monad laws.
\end{itemize}

We call our type class ``lawful monad'' because the monad laws are required to
hold. To instantiate this definition, we must supply the type constructor
\li{m}, suitable \li{bind} and \li{pure} operators, and proofs of the monad
laws.

Lean includes a predefined concept of monads, which is essentially equivalent
to the above but is more complicated. In particular, Lean distributes the
definition over a syntactic type class \li{monad} and a semantic type class
\li{is_lawful_monad}.

\section{No Effects}
\label{sec:no-effects}

Lean's constant \li|id {α : Type} : α → α| is defined as the identity
function \li{λx, x}. The identity type constructor is obtained by taking
\li{α := Type}. We can register it as a monad:

\lstinputlisting[linerange=id_monad-q]{../lean/love06_monads_demo_master.lean}
%
The \emph{identity monad} is the simplest monad possible. It provides a simple
box, with a single value in it, without any effect. It plays a similar role as
0 in additive arithmetic. We can think of the other monads as variations of it;
for example, the option monad is an identity monad enriched with a special
\li{option.none} value representing an error state.

\section{Exceptions}
\label{sec:exceptions}

As we saw above, the option monad provides a simple kind of exceptions. The
following code shows how to register \li{option : Type → Type} as a lawful monad:
%
\lstinputlisting[linerange=option_monad-q]{../lean/love06_monads_demo_master.lean}
%
The registration process requires us to provide five components:\
the \li{pure} and \li{bind} operations and the proofs of the three monad laws.
For the first and second components of the record, we use the \li{@} syntax to
make the type arguments explicit, in agreement with the format expected by
\li{has_pure} and \li{has_bind}. The three proofs are straightforward.

Beyond the standard operations, it can be useful to throw and catch exceptions.
This can be implemented as follows:
%
\lstinputlisting[linerange=option_throw_catch-q]{../lean/love06_monads_demo_master.lean}
%
The \li{option.throw} operation raises an exception, leaving the program in an
error state (\li{option.none}). The \li{option.catch} operation can be used
to recover from an earlier exception. If the program is currently in an error
state, \li{option.catch} invokes some exception-handling code (its second
argument). This code might in turn raise a new exception. If \li{option.catch}
is applied to a normal state (of the form \li{option.some a}), nothing happens.

As a convenient alternative to \li{option.}\allowbreak\li{catch ma ma'}, Lean
supports the syntax \li{ma.catch ma'}. Here is a schematic example that
demonstrates throwing and catching with this syntax:
%
\begin{lstlisting}
do {
  …,
  if … then
    option.throw
  else
    … }
.catch do {
  … }
\end{lstlisting}
%
The corresponding Java code would look as follows:
%
{\tabletsmall
\begin{lstlisting}[language=minijavaandc]
try {
    …
    if (…) {
        throw new UnknownException();
    } else {
        …
    }
} catch (UnknownException e) {
    …
}
\end{lstlisting}}

A more idiomatic approach is to register \li{option.catch} as the option type's
``or else'' operator \li{<|>}:
%
\lstinputlisting[linerange=option_has_orelse-q]{../lean/love06_monads_demo_master.lean}
%
This enables us to write
%
\begin{lstlisting}
do {
  …,
  if … then
    option.throw
  else
    … }
<|>
do {
  … }
\end{lstlisting}
%
Monads equipped with \li{<|>} are called \emph{alternative monads}.

Options cater for only one kind of error state. A more general abstraction,
called \emph{error monad}, supports different errors, as with the exceptions of
Java and other programming languages.

\section{Mutable State}
\label{sec:mutable-state}

The \emph{state monad} provides an abstraction corresponding to a mutable
state. For some programming languages, the compiler can detect the use of the
state monad and translate programs using them to more efficient imperative
programs.

Admittedly, ``abstraction corresponding to a mutable state'' may sound somewhat
abstract, so let us consider a semiconcrete example. If you have some
experience with functional programming, you probably at some point or other
have written code that looks very much like this fragment:

\begin{lstlisting}
def welcome_new_user (user_name : string) (ctxt : context) :
  (ℕ × string) × context :=
let
  (user, ctxt') := create_user user_name ctxt,
  (password, ctxt'') := generate_temporary_password user ctxt',
  (ok, ctxt''') := send_unencrypted_email user password ctxt''
in
  ((user, password), ctxt''')
\end{lstlisting}
%
(It is very important to send the password in an unencrypted email, and to
ignore the \li{ok} status of the function.) The function takes some global
state or context as input and invokes three functions in turn, each of which
takes a context value and returns both some data and a new context. The context
is effectively \emph{threaded through} the program. This allows us to have a
mutable state in a programming language without side effects.

The above approach is error-prone---it is all too easy to forget one prime
(\li{'}) and pass the wrong context to a function---as well as cluttered by all
the context variables. What if we could simply write the following instead?

\begin{lstlisting}
def welcome_new_user₂ (user_name : string) :
  context → (ℕ × string) × context :=
do
  user ← create_user user_name,
  password ← generate_temporary_password user,
  ok ← send_unencrypted_email user password,
  pure (user, password)
\end{lstlisting}
%
This is what the state monad provides.

The underlying type constructor captures the concept of computations or actions
over states of type \li{σ} and with return values of type \li{α}:%
\footnote{This type constructor is traditionally called \texttt{State} or
\texttt{state}, but these names are awfully confusing. In this case, it seems
preferable to honor tradition in the breach rather than in the observance.}
%
\lstinputlisting[linerange=action-q]{../lean/love06_monads_demo_master.lean}
%
For a given type \li{σ}, we have that \li{action σ : Type → Type} is a monad.
The type \li{σ} abstracts over the exact memory layout. We could use tuples or
lists to represent memory, for example, and instantiate the abstract state
\li{σ} accordingly.

A stateful action is a function that takes some state and returns both a value
and some new state. The \li{σ →} part of \hbox{\li{action}'s} definition
gives the old state; the left component of the cartesian product, \li{α},
gives the result of the computation; and the right component of the product,
\li{σ}, gives the new state. Thus, the state is implicitly threaded through
the program. As with other effectful programs, the \li{do} notation only
exposes the data---the value of type~\li{α}---and conceals the effect---the old
and new \li{σ} states.

The case where \li{σ := unit}, a type of cardinality one (similar to \li{void}
in Java or C) whose unique value is written \li{()}, corresponds to the
identity monad: The type \li{unit → α × unit} is isomorphic to \li{α}. This
intuition can guide us when defining \li{pure} and \li{bind}.

We start by defining basic operations:\ two operations, \li{read} and
\li{write}, to access the memory, and the standard operations \li{bind} and
\li{pure}:

\lstinputlisting[linerange=action_monad_defs-q]{../lean/love06_monads_demo_master.lean}
%
The \li{read} operation simply returns the current state \li{s} (in the first
pair component) and leaves the state unchanged (in the second pair component).
The \li{write} operation replaces the state \li{s} with \li{t} and returns
\li{()}. The \li{pure} operation returns the current state \li{s} unchanged
tupled together with the given value \li{a}. The \hbox{\li{bind}} operation
passes the initial state to the \li{f} argument, yielding a result \li{a} and a
new state \li{t}. These are passed to \li{g}, which returns a new result and a
new state.

Registering the state monad as a lawful monad is similar as for \li{option},
but we need functional extensionality (\li{funext}):
To prove \li{f = g}, it is sufficient to show \li{∀x, f x = g x}.

\lstinputlisting[linerange=action_monad_register-q]{../lean/love06_monads_demo_master.lean}

As a concrete example, the following program removes all elements that are
smaller than a previous element in the list, leaving us with a list of
increasing elements. The maximal element is stored as the state~\li{σ}.

\lstinputlisting[linerange=diff_list-q]{../lean/love06_monads_demo_master.lean}
%
Notice how the state is accessed by \li{read} and \li{write}.

To execute the program, we must supply an initial state. The last state is
returned along with the resulting list. It corresponds to the largest element
encountered in the list or the start state. Thus, the commands

\lstinputlisting[linerange=diff_list_eval-q]{../lean/love06_monads_demo_master.lean}
%
produce the output

\begin{lstlisting}[language=]
([1, 2, 3], 3)
([1, 2, 3, 4, 5], 5)
\end{lstlisting}

\section{Nondeterminism}
\label{sec:nondeterminism}

Whereas the option monad stores zero or one \li{α} values and the identity and
state monads store exactly one \li{α} value, the \emph{set monad} provides an
arbitrary, possibly infinite number of \li{α} values. This is useful to model
nondeterminism, as sets of possible behaviors.

Lean's type \li{set α} is defined as \li{α → Prop}. In other words, a set is
identified with its characteristic predicate. Familiar operators such as
the empty set (\li{∅}), the universal set (\li{set.univ}), union (\li{∪}),
intersection (\li{∩}), and membership (\li{∈}) are supported, as well as
traditional curly brace notations such as \li${a}$, \li${a, b}$, and
\li${x |$ \li$p x}$. Many set constructs can be simplified by \li{simp}.

The \li{set} type constructor can be registered as a lawful monad as follows:

\lstinputlisting[linerange=set_monad-q]{../lean/love06_monads_demo_master.lean}
%
The \li{pure} operation simply puts the given value \li{a} in a singleton set
\li${a}$. The \li{bind} operation calls \li{f} on all values in the set \li{A}
and returns the union of all the results. For example, if \li$A := {3, 8}$ and
\li$f := (λa, {a, a + 1})$, then \li|set.bind A f| equals
\hbox{\li|{3, 4, 8, 9}|.} The last proof relies on \emph{set extensionality},
which states that two sets that contain the same elements must be equal:
%
\[\hbox{\lic$set.ext {α : Type} {A B : set α}$ \lic{:} \lic|(∀x, x ∈ A ↔ x ∈ B) → A = B|}\]
%
Another noteworthy point is the use of the \li{tautology} tactic. The
goal's target is
\ifdefined\TABLET
  \li{∀x, (∃a, (∃a_1, a_1 ∈ m ∧ a ∈ f a_1) ∧ x ∈ g a) ↔ (∃a, a ∈ m ∧ ∃a_1, a_1 ∈ f a ∧ x ∈ g a_1)},
\else
  \hbox{\li{∀x,}}
  \hbox{\li{(∃a, (∃a_1, a_1 ∈ m ∧ a ∈ f a_1) ∧ x ∈ g a) ↔ (∃a, a ∈ m ∧ ∃a_1, a_1 ∈ f a}}
  \hbox{\li{∧ x ∈ g a_1)}},
\fi
where the two sides of \li{↔} are the same except for the placement of the
existential quantifiers (and, confusingly, the names of the bound variables).
This ugly proposition could be proved by a tedious sequence of introduction and
elimination, but we deserve more automation.

\section{Tautology Tactic}
\label{sec:tautology-tactic}

\subsection*{tautology}

The \li{tautology} tactic performs elimination of the logical symbols \li{∧},
\li{∨}, \li{↔}, and \li{∃} in hypotheses and introduction of \li{∧}, \li{↔}, and
\li{∃} in the target, until all the emerging subgoals can be trivially
proved (e.g., by \li{refl}).

\section{A Generic Algorithm: Iteration over a List}
\label{sec:a-generic-algorithm-iteration-over-a-list}

As a final example, we consider a generic effectful program \li{mmap} that
iterates over a list and applies a function \li{f} to each element. The
definition is recursive:

\lstinputlisting[linerange=mmap_def-q]{../lean/love06_monads_demo_master.lean}
%
Notice that the function returns a single \li{m} value containing a list and
not a list of \li{m} values. Try to work out why it is well typed and has the
desired behavior.

The \li{mmap} function distributes over the append operator \li{++}. The \li{do}
notation is useful not only for defining functions but also for stating their
properties:

\lstinputlisting[linerange=mmap_append-q]{../lean/love06_monads_demo_master.lean}

Here is an example of how we could use \li{mmap}:

\lstinputlisting[linerange=nths-q]{../lean/love06_monads_demo_master.lean}
%
The function \li{nths xss n} extracts the \li{(n + 1)}st element of each list in
\li{xss}. It fails with \li{option.none} if one of the list is not long enough.
Running

\lstinputlisting[linerange=nths_eval-q]{../lean/love06_monads_demo_master.lean}
%
returns \li{option.some [13, 23, 33]}.

Lean already includes a function called \li{list.mmap} corresponding to our
\li{mmap}.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Notations}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|do| & indicates the start of a monadic program \\
\li|let| & introduces a local definition in a monad \\
\li$<|>$ & tries the left-hand side first; tries the right-hand side on~failure \\
\li|>>=| & composes monadic computations \\
\end{xltabular}

\subsection*{Lemma}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|set.ext| & set extensionality \\
\end{xltabular}

\subsection*{Tactic}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|tautology| & proves tautologies involving the basic logical symbols \\
\end{xltabular}

\endgroup
