git.iko.soy/Idris-dev
on master help sign in
Remove the DependentPair typeclass.
77ea792Matus Tejiscak
libs/prelude/Builtins.idr+9−2
compare with master
unifiedsplit
@@ -3,13 +3,20 @@
3%access public
3%access public
4%default total
4%default total
5
5
6−||| Dependent pairs, in their internal representation.
6+||| Dependent pairs, in their internal representation
7−||| Nothing is erased in this variant; for alternatives see Prelude.Pairs.
8||| @ a the type of the witness
7||| @ a the type of the witness
9||| @ P the type of the proof
8||| @ P the type of the proof
10data Pair : (a : Type) -> (P : a -> Type) -> Type where
9data Pair : (a : Type) -> (P : a -> Type) -> Type where
11 pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
10 pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
12
11
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+
13||| The eliminator for the empty type.
20||| The eliminator for the empty type.
14FalseElim : _|_ -> a
21FalseElim : _|_ -> a
15
22
libs/prelude/Prelude/Pairs.idr+2−22
@@ -5,28 +5,8 @@ module Prelude.Pairs
5
5
6||| Dependent pair where the first field is erased.
6||| Dependent pair where the first field is erased.
7data Exists : {a : Type} -> (P : a -> Type) -> Type where
7data 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
9
9
10||| Dependent pair where the second field is erased.
10||| Dependent pair where the second field is erased.
11data Subset : (a : Type) -> (P : a -> Type) -> Type where
11data Subset : (a : Type) -> (P : a -> Type) -> Type where
12− element : (x : a) -> .(pf : P x) -> Subset a P
12+ element : .{P : a -> Type} -> (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