@@ -158,6 +158,74 @@ value of type ``Type``).
158158 Nil : Vect Z a
159159 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
160160
161+The signature of type constructors may use dependent types
162+
163+.. code:: idris
164+
165+ data DPair : (a : Type) -> (a -> Type) -> Type where
166+ MkDPair : {P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
167+
168+Records
169+~~~~~~~
170+
171+There is a special syntax for data types with one constructors and
172+multiple fields.
173+
174+.. code:: idris
175+
176+ record A a where
177+ constructor MkA
178+ foo, bar : a
179+ baz : Nat
180+
181+This defines a constructor as well as getter and setter function for
182+each field.
183+
184+.. code:: idris
185+
186+ MkA : a -> a -> Nat -> A a
187+ foo : A a -> a
188+ set_foo : a -> A a -> A a
189+
190+The types of record fields may depend on the value of other fields
191+
192+.. code:: idris
193+
194+ record Collection a where
195+ constructor MkCollection
196+ size : Nat
197+ items : Vect size a
198+
199+Setter functions are only provided for fields that do not use dependant
200+types. In the example above neither ``set_size`` nor ``set_items`` are
201+defined.
202+
203+
204+Co-data
205+~~~~~~~
206+
207+Inifinite data structures can be introduced with the ``codata``
208+keyword.
209+
210+.. code:: idris
211+
212+ codata Stream : Type -> Type where
213+ (::) a -> Stream a -> Stream a
214+
215+This is syntactic sugar for
216+
217+.. code:: idris
218+
219+ data Stream : Type -> Type where
220+ (::) a -> Delayed Infinite (Stream a) -> Stream a
221+
222+Every occurence of the the defined type in a constructor argument will
223+be wrapped in the ``Delayed Infinite`` type constructor. This has the
224+effect of delaying the evaluation of the second argument when the data
225+constructor is applied. The argument is only evaluated when we pattern
226+match against the constructor.
227+
228+
161229Operators
162230---------
163231