@@ -23,7 +23,17 @@ Which declare and define the datatype as the names suggest.
2323 :height: 246px
2424 :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
2525
26−Here is a simple example constructing a boolean type:
26+.. list-table::
27+
28+ * - As a first example, the following boolean-like type can be constructed. When the compiler has run it will be available to us as if we had compiled it in the usual way:
29+ - .. code-block:: idris
30+
31+ λΠ> :printdef Two
32+ data Two : Type where
33+ F : Two
34+ T : Two
35+
36+This was generated by the following code:
2737
2838.. code-block:: idris
2939
@@ -42,15 +52,7 @@ Here is a simple example constructing a boolean type:
4252
4353.. list-table::
4454
45− * - This type is now available to us as if we had compiled it in the usual way:
46− - .. code-block:: idris
47−
48− λΠ> :printdef Two
49− data Two : Type where
50− F : Two
51− T : Two
52−
53− * - The constructors are T and F:
55+ * - The constructors T and F can be called as would be expected:
5456 - .. code-block:: idris
5557
5658 λΠ> F
@@ -76,7 +78,23 @@ Which declare and define the function as the names suggest.
7678 :height: 246px
7779 :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
7880
79−We can now add some function definitions to the above datatype:
81+Note: FunClause - holds a 'let' clause, the left hand side (lhs) and right hand side (rhs) must have the same type. TT does not have 'where' clauses because they are desugared out.
82+
83+.. list-table::
84+
85+ * - Some function definitions can now be added to the above datatype. This is what they will look like:
86+ - .. code-block:: idris
87+
88+ λΠ> :printdef perm1
89+ perm1 : Two -> Two
90+ F = F
91+ T = T
92+ λΠ> :printdef perm2
93+ perm2 : Two -> Two
94+ F = F
95+ T = T
96+
97+This was generated with the following code:
8098
8199.. code-block:: idris
82100
@@ -98,18 +116,6 @@ We can now add some function definitions to the above datatype:
98116
99117.. list-table::
100118
101− * - Here are the functions:
102− - .. code-block:: idris
103−
104− λΠ> :printdef perm1
105− perm1 : Two -> Two
106− F = F
107− T = T
108− λΠ> :printdef perm2
109− perm2 : Two -> Two
110− F = F
111− T = T
112−
113119 * - This is what happens when we call the functions:
114120 - .. code-block:: idris
115121
@@ -118,7 +124,21 @@ We can now add some function definitions to the above datatype:
118124 λΠ> perm2 T
119125 F T : Two
120126
121−Here is an example with parameters:
127+So far these datatypes and functions could have been written, statically, in the usual way. However, it is possible to imagine situations where we may need a lot of functions to be generated automatically at compile time. For example, if we extend this Boolean datatype to a datatype with more simple constructors (a finite set), we could generate a function for every possible permutation of that datatype back to itself.
128+
129+A Different Example which has Type Parameters
130+---------------------------------------------
131+
132+.. list-table::
133+
134+ * - Here is an example of a datatype with type parameters:
135+ - .. code-block:: idris
136+
137+ data N : Nat -> Type where
138+ MkN : N x
139+ MkN' : (x : Nat) -> N (S x)
140+
141+This was produced by the following code:
122142
123143.. code-block:: idris
124144
@@ -138,15 +158,7 @@ Here is an example with parameters:
138158
139159 %runElab addData
140160
141−So this declares and defines the following data structure 'N' with a constructor 'MkN' which can have an implicit or an explicit Nat argument.
142−
143−.. code-block:: idris
144−
145− data N : Nat -> Type where
146− MkN : N x
147− MkN' : (x : Nat) -> N (S x)
148−
149−Which can be used like this:
161+So this declares and defines the following data structure 'N' with a constructor 'MkN' which can have an implicit or an explicit Nat argument. Which can be used like this:
150162
151163.. code-block:: idris
152164