@@ -20,31 +20,11 @@ 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)
23+* `UPair` and `Sigma` have been renamed `UniquePair` and `DepPair`
24+ respectivly.
25+* Accessor functions for dependent pairs have been renamed to bring them into
26+ line with standard accessor functions for pairs. The function `getWitness`
27+ is now `fst`, and `getProof` is `snd`.
4828
4929New in 0.10:
5030============