@@ -158,6 +158,74 @@ value of type ``Type``).
158 Nil : Vect Z a
158 Nil : Vect Z a
159 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
159 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
161+The signature of type constructors may use dependent types
165+ data DPair : (a : Type) -> (a -> Type) -> Type where
166+ MkDPair : {P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
171+There is a special syntax for data types with one constructors and
181+This defines a constructor as well as getter and setter function for
186+ MkA : a -> a -> Nat -> A a
188+ set_foo : a -> A a -> A a
190+The types of record fields may depend on the value of other fields
194+ record Collection a where
195+ constructor MkCollection
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
207+Inifinite data structures can be introduced with the ``codata``
212+ codata Stream : Type -> Type where
213+ (::) a -> Stream a -> Stream a
215+This is syntactic sugar for
219+ data Stream : Type -> Type where
220+ (::) a -> Delayed Infinite (Stream a) -> Stream a
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.