git.iko.soy/Idris-dev
on master help sign in
Removal of deprecated functions for Pairs.
3f7bb1cJan de Muijnck-Hughes
libs/prelude/Builtins.idr−8
compare with master
unifiedsplit
@@ -51,14 +51,6 @@ namespace Builtins
51 data DPair : (a : Type) -> (P : a -> Type) -> Type where
51 data DPair : (a : Type) -> (P : a -> Type) -> Type where
52 MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
52 MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
53
53
54− Sigma : (a : Type) -> (P : a -> Type) -> Type
55− Sigma wit prf = DPair wit prf
56− %deprecate Sigma "This name is being deprecated in favour of `DPair`."
57−
58− MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DPair a P
59− MkSigma wit prf = MkDPair wit prf
60− %deprecate MkSigma "This constructor is being deprecated in favour of `MkDPair`."
61−
62||| The empty type, also known as the trivially false proposition.
54||| The empty type, also known as the trivially false proposition.
63|||
55|||
64||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope.
56||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope.
libs/prelude/Prelude/Pairs.idr−8
@@ -41,13 +41,5 @@ using (a : Type, P : a -> Type)
41 snd : (x : DPair a P) -> P (fst x)
41 snd : (x : DPair a P) -> P (fst x)
42 snd (x ** pf) = pf
42 snd (x ** pf) = pf
43
43
44− getWitness : DPair a P -> a
45− getWitness = fst
46− %deprecate DPair.getWitness "This is being deprecated in favour of `fst`."
47−
48− getProof : (x : DPair a P) -> P (fst x)
49− getProof = snd
50− %deprecate DPair.getProof "This is being deprecated in favour of `snd`."
51−
52 -- Polymorphic (interface-based) projections have been removed
44 -- Polymorphic (interface-based) projections have been removed
53 -- because type-directed name disambiguation works better.
45 -- because type-directed name disambiguation works better.