@@ -81,6 +81,9 @@ Minor language changes
81 which may be inferred from the definition of the hole).
81 which may be inferred from the definition of the hole).
82* Programs with holes can now be compiled.
82* Programs with holes can now be compiled.
83 Attempting to evaluate an expression with a hole results in a run time error.
83 Attempting to evaluate an expression with a hole results in a run time error.
84+* Dependent pairs now can be specified using a telescope-style syntax, without
85+ requirement of nesting, e.g. it is possible to now write the following:
86+ (a : Type ** n : Nat ** Vect n a)
85External Dependencies
88External Dependencies
86---------------------
89---------------------
@@ -101,9 +104,6 @@ New in 0.10:
101 Where `CATS` is a whitespace separated list of categoriese. Default is for
104 Where `CATS` is a whitespace separated list of categoriese. Default is for
102 all categories to be logged.
105 all categories to be logged.
103* New flag `--listlogcats` to list logging categories.`
106* New flag `--listlogcats` to list logging categories.`
104−* Dependent pairs now can be specified using a telescope-style syntax, without
105− requirement of nesting, e.g. it is possible to now write the following:
106− (a : Type ** n : Nat ** Vect n a)
108New in 0.9.20:
108New in 0.9.20:
109==============
109==============