Restored usage annotation.
commit006bd17d86990ed26bce927480fe2a59196a229c
authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk>
dateThu 28 Jan 2016, 20:53 (11 years ago)
parent66a97ec
libs/prelude/Builtins.idr+4
@@ -33,6 +33,10 @@ namespace Builtins
3333 ||| @b the right element of the pair
3434 MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
3535
36+ -- Usage hints for erasure analysis
37+ %used MkUniquePair a
38+ %used MkUniquePair b
39+
3640 UPair : (A : AnyType) -> (B : AnyType) -> AnyType
3741 UPair a b = UniquePair a b
3842 %deprecate UPair "This name is being deprecated in favour of `UniquePair`"