Make additions public and require totality
commite87a7ae407b59d24d72407322a93c5985664148a
authorMelvar Chen <Melvar.Chen@googlemail.com>
dateTue 25 Jun 2013, 18:02 (13 years ago)
parentc5979f4
lib/Data/HVect.idr+3
@@ -2,6 +2,9 @@ module Data.HVect
22
33import Data.Vect
44
5+%access public
6+%default total
7+
58using (k : Nat, ts : Vect Type k)
69 data HVect : Vect Type k -> Type where
710 Nil : HVect []
lib/Data/Vect.idr+3
@@ -2,6 +2,9 @@ module Data.Vect
22
33import Language.Reflection
44
5+%access public
6+%default total
7+
58--------------------------------------------------------------------------------
69-- Elem
710--------------------------------------------------------------------------------