Merge pull request #4023 from msmorgan/feature/pairs-implicit
add Data.Pairs.Implicit for converting erased pairs
commit6e066f7a27e83f2fcf1934a6632262a1271138ca
authorNiklas Larsson <metaniklas@gmail.com>
dateSun 27 Aug 2017, 01:34 (9 years ago)
parent14148f659d2a1f
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