add Data.Pairs.Implicit for converting erased pairs
The conversions are performed by the functions `evidence` and `element`.
commit59d2a1f2113354d306c046ca3e0d38b37614885f
authorMichael Morgan <michael.morgan@mind-over-data.com>
dateFri 25 Aug 2017, 19:53 (9 years ago)
parente2843b0
libs/contrib/Data/Pairs/Implicit.idrnew file+13
@@ -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,
2424 Data.SortedMap, Data.SortedSet,
2525 Data.CoList, Data.Storable,
2626 Data.List.Zipper,
27+ Data.Pairs.Implicit,
2728
2829 Decidable.Decidable, Decidable.Order,
2930