git.iko.soy/Idris-dev
on master help sign in
Restored usage annotation.
006bd17Jan de Muijnck-Hughes
libs/prelude/Builtins.idr+4
compare with master
unifiedsplit
@@ -33,6 +33,10 @@ namespace Builtins
33 ||| @b the right element of the pair
33 ||| @b the right element of the pair
34 MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
34 MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
35
35
36+ -- Usage hints for erasure analysis
37+ %used MkUniquePair a
38+ %used MkUniquePair b
39+
36 UPair : (A : AnyType) -> (B : AnyType) -> AnyType
40 UPair : (A : AnyType) -> (B : AnyType) -> AnyType
37 UPair a b = UniquePair a b
41 UPair a b = UniquePair a b
38 %deprecate UPair "This name is being deprecated in favour of `UniquePair`"
42 %deprecate UPair "This name is being deprecated in favour of `UniquePair`"