@@ -20,31 +20,11 @@ Minor language changes
21* The '[static]' annotation is changed to '%static' to be consistent with the
21* The '[static]' annotation is changed to '%static' to be consistent with the
22 other annotations.
22 other annotations.
23−* Added '%auto_implicits' directive. The default is '%auto_implicits on'.
23+* `UPair` and `Sigma` have been renamed `UniquePair` and `DepPair`
24− Placing '%auto_implicits off' in a source file means that after that
24+ respectivly.
25− point, any implicit arguments must be bound, e.g.:
25+* Accessor functions for dependent pairs have been renamed to bring them into
26− append : {n,m,a:_} -> Vect n a -> Vect m a -> Vect (n + m) a
26+ line with standard accessor functions for pairs. The function `getWitness`
27−
27+ is now `fst`, and `getProof` is `snd`.
28− Only names which are used explicitly in the type need to be bound, e.g.:
29− Here : {x, xs : _} -> Elem x (x :: xs)
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
35− You can still implicitly bind with 'using':
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)
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:
46− using (xs : Vect n a)
47− bad : Elem x xs -> Elem x (y :: xs)
49New in 0.10:
29New in 0.10:
50============
30============