lysa/ru/chapters/2/3-idris.ltx

\s{Idris}

This section provides a ``working example'' of the above in Idris. If you don't
know what that is, you are a bad person. Go back and read \cref{intro-idris}!

Open up an Idris prompt, and enter \code{:type True}. That is basically asking
Idris ``what type of thing is \truenm?'' Idris will tell you. Also do the same
thing for \falsenm. Here's what happens when I do it:

\begin{lstlisting}
Idris> :type True
Prelude.Bool.True : Bool
Idris> :type False
Prelude.Bool.False : Bool
\end{lstlisting}

If you ask Idris what the type of \code{True} or \code{False} is, it will tell
you that they are \code{Bool}s.\footnote{For the most part, you can ignore all
  the weird stuff on the left-hand-side, for the time being. For instance, when
  I ran \code{:type True}, Idris switched \code{True} to
  \code{Prelude.Bool.True}. These are odd caveats of Idris's syntax, which I
  don't have time to explain right now. We'll get to them later, I promise.}
You're probably thinking ``what the hell is a \code{Bool}?'' \code{Moreover, why
  the hell is this guy printing all this stuff in monospace}? Well, explaining
this sorta stuff, that's what I'm here for. \code{Bool} is short for Boolean,
which is what this chapter is about.

The reason I'm printing stuff \code{in monospace} is to say ``hey, this is
code.'' More importantly, printing stuff in monospace eschews some formatting
flukes caused by variable-width text. In normal paragraph text, these flukes are
fine --- they are even helpful --- but they cause some ambiguities in code. For
that reason, the standard thing to do is to write code in monospace.

In Idris, and in most programming languages, the $\land$ operator is replaced
with \code{\&\&}. We know that, in Idris \truenm\ and \falsenm\ are both Boolean
values. What about $\true \land \false$?

\begin{lstlisting}
Idris> :type (True && False)
True && Delay False : Bool
\end{lstlisting}

\xti{So, wait, \truenm\ and \falsenm\ are both Boolean values, but
  $\true \land \false$ is also a Boolean value?}

Yes, Timmy, now try to keep up.

Now, from the explanation of $\land$ in \cref{s: Basic Logic},
$\true \land \false$ should only be true if both \truenm\ and \falsenm\ are
\truenm. Well, that's obviously not the case, so $\true \land \false$ should
turn out to be \falsenm, right? Let's see!

\begin{lstlisting}
Idris> True && False
False : Bool
\end{lstlisting}

What about $\lor$?  In Idris --- and most programming languages --- $\lor$ is
replaced with \code{||}.

\begin{lstlisting}
Idris> True || False
True : Bool
\end{lstlisting}