@@ -0,0 +1,83 @@
1+\section{Language Overview}
3+\subsection{Primitive Types}
5+\Idris{} defines several primitive types: \tTC{Int}, \tTC{Integer} and
6+\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for
7+text manipulation, and \tTC{Ptr} which represents foreign pointers.
8+There are also several data types declared in the library, including
9+\tTC{Bool}, with values \tDC{True} and \tDC{False}.
10+We can declare some constants with these types. Enter the following
11+into a file \texttt{prims.idr} and load it into the \Idris{} interactive
12+environment by typing \texttt{idris prims.idr}:
14+\begin{SaveVerbatim}{constprims}
22+foo = "Sausage machine";
33+An \Idris{} file consists of an optional module declaration (here
34+\texttt{module prims}) followed by an optional list of imports (none here,
35+however \Idris{} programs can consist of several modules, and the definitions
36+in each module each have their own namespace, as we will discuss shortly) and a
37+collection of declarations and definitions. Each definition must have a type
38+declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc). Each
39+component is separated by a semi-colon.
41+A library module \texttt{prelude} is automatically imported by every \Idris{} program,
42+including facilities for IO, arithmetic, data structures and various common
43+functions. The prelude defines several arithmetic and comparison operators,
44+which we can use at the prompt. Evaluating things at the prompt gives an
45+answer, and the type of the answer. For example:
47+\begin{SaveVerbatim}{promptprim}
57+All of the usual arithmetic and comparison operators are defined for the primitive
58+types. They are overloaded using type classes, as we will discuss in section
59+\ref{sec:classes} and can be extended to work on user defined types.
60+Boolean expressions can be tested with the \texttt{if...then...else} construct:
62+\begin{SaveVerbatim}{ifthenelse}
64+*prims> if (x==6*6+6) then "The answer!" else "Not the answer"
65+"The answer!" : String
70+\subsection{Data Types}
74+\subsection{Dependent Types}
76+\subsubsection{Vectors}
78+\subsubsection{The Finite Sets}
80+\subsubsection{Implicit Arguments}
82+\subsection{Modules and Namespaces}