git.iko.soy/Idris-dev
on master help sign in
add Data.Pairs.Implicit for converting erased pairs
59d2a1fMichael Morgan
libs/contrib/Data/Pairs/Implicit.idrnew file+13
compare with master
unifiedsplit
@@ -0,0 +1,13 @@
1+||| Implicit conversions for erased dependent pairs.
2+module Data.Pairs.Implicit
3+
4+%access public export
5+%default total
6+
7+||| Convert an Evidence to its proof.
8+implicit evidence : (x : Exists p) -> p (getWitness x)
9+evidence = getProof
10+
11+||| Convert an Element to its value (a.k.a. witness).
12+implicit element : Subset a p -> a
13+element = getWitness
libs/contrib/contrib.ipkg+1
@@ -24,6 +24,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
24 Data.SortedMap, Data.SortedSet,
24 Data.SortedMap, Data.SortedSet,
25 Data.CoList, Data.Storable,
25 Data.CoList, Data.Storable,
26 Data.List.Zipper,
26 Data.List.Zipper,
27+ Data.Pairs.Implicit,
27
28
28 Decidable.Decidable, Decidable.Order,
29 Decidable.Decidable, Decidable.Order,
29
30