git.iko.soy/Idris-dev
on master help sign in
Remove the DependentPair typeclass.
commit77ea792f3e3588e514c76d8f4a2a11400d0cbcf2 authorMatus Tejiscak <ziman@functor.sk> dateThu 22 May 2014, 18:41 (12 years ago) parent9781c94
2 files changed+11−24
compare with master
unifiedsplit
libs/prelude/Builtins.idr+9−2 libs/prelude/Prelude/Pairs.idr+2−22
libs/prelude/Builtins.idr+9−2
@@ -3,13 +3,20 @@
33%access public
44%default total
55
6−||| Dependent pairs, in their internal representation.
7−||| Nothing is erased in this variant; for alternatives see Prelude.Pairs.
6+||| Dependent pairs, in their internal representation
87||| @ a the type of the witness
98||| @ P the type of the proof
109data Pair : (a : Type) -> (P : a -> Type) -> Type where
1110 pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
1211
12+||| The first projection from a dependent pair
13+getWitness : {P : a -> Type} -> Pair a P -> a
14+getWitness (a ** v) = a
15+
16+||| The second projection from a dependent pair
17+getProof : {P : a -> Type} -> (s : Pair a P) -> P (getWitness s)
18+getProof (a ** v) = v
19+
1320||| The eliminator for the empty type.
1421FalseElim : _|_ -> a
1522
libs/prelude/Prelude/Pairs.idr+2−22
@@ -5,28 +5,8 @@ module Prelude.Pairs
55
66||| Dependent pair where the first field is erased.
77data Exists : {a : Type} -> (P : a -> Type) -> Type where
8− witness : .{x : a} -> (pf : P x) -> Exists P
8+ witness : .{P : a -> Type} -> .{x : a} -> (pf : P x) -> Exists P
99
1010||| Dependent pair where the second field is erased.
1111data Subset : (a : Type) -> (P : a -> Type) -> Type where
12− element : (x : a) -> .(pf : P x) -> Subset a P
13−
14−||| Class of dependent pair constructors.
15−class DependentPair f where
16− ||| Project the first field from a dependent pair.
17− getWitness : f a P -> a
18−
19− ||| Project the second field from a dependent pair.
20− getProof : (x : f a P) -> P (getWitness x)
21−
22−instance DependentPair Pair where
23− getWitness (pair x pf) = x
24− getProof (pair x pf) = pf
25−
26−instance DependentPair Exists where
27− getWitness (witness x pf) = x
28− getProof (witness x pf) = pf
29−
30−instance DependentPair Subset where
31− getWitness (element x pf) = x
32− getProof (element x pf) = pf
12+ element : .{P : a -> Type} -> (x : a) -> .(pf : P x) -> Subset a P