@@ -20,6 +20,31 @@ Minor language changes
2020
2121* The '[static]' annotation is changed to '%static' to be consistent with the
2222 other annotations.
23+* Added '%auto_implicits' directive. The default is '%auto_implicits on'.
24+ Placing '%auto_implicits off' in a source file means that after that
25+ point, any implicit arguments must be bound, e.g.:
26+ append : {n,m,a:_} -> Vect n a -> Vect m a -> Vect (n + m) a
27+
28+ Only names which are used explicitly in the type need to be bound, e.g.:
29+ Here : {x, xs : _} -> Elem x (x :: xs)
30+
31+ In 'Here', there is no need to bind any of the variables in the type of
32+ 'xs' (it could be e.g. List a or Vect n a; 'a' and 'n' will still be
33+ implicitly bound).
34+
35+ You can still implicitly bind with 'using':
36+
37+ using (xs : Vect _ _)
38+ data Elem : {a, n : _} -> a -> Vect n a -> Type where
39+ Here : {x : _} -> Elem x (x :: xs)
40+ There : {x, y : _} -> Elem x xs -> Elem x (y :: xs)
41+
42+ However, note that *only* names which appear in *both* the using block
43+ *and* the type being defined will be implicitly bound. The following will
44+ therefore fail because 'n' isn't implicitly bound:
45+
46+ using (xs : Vect n a)
47+ bad : Elem x xs -> Elem x (y :: xs)
2348* `Sigma` has been renamed to `DPair`.
2449* Accessor functions for dependent pairs have been renamed to bring them into
2550 line with standard accessor functions for pairs. The function `getWitness`