git.iko.soy/Idris-dev
on master help sign in
Removal of deprecated functions for Pairs.
commit3f7bb1ce6d3974a39035ca9294f84ba128615a14 authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateFri 10 Nov 2017, 11:11 (9 years ago) parent61ce9a5
2 files changed−16
compare with master
unifiedsplit
libs/prelude/Builtins.idr−8 libs/prelude/Prelude/Pairs.idr−8
libs/prelude/Builtins.idr−8
@@ -51,14 +51,6 @@ namespace Builtins
5151 data DPair : (a : Type) -> (P : a -> Type) -> Type where
5252 MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
5353
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−
6254||| The empty type, also known as the trivially false proposition.
6355|||
6456||| 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)
4141 snd : (x : DPair a P) -> P (fst x)
4242 snd (x ** pf) = pf
4343
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−
5244 -- Polymorphic (interface-based) projections have been removed
5345 -- because type-directed name disambiguation works better.