git.iko.soy/Idris-dev
on master help sign in
Make additions public and require totality
e87a7aeMelvar Chen
lib/Data/HVect.idr+3
compare with master
unifiedsplit
@@ -2,6 +2,9 @@ module Data.HVect
2
2
3import Data.Vect
3import Data.Vect
4
4
5+%access public
6+%default total
7+
5using (k : Nat, ts : Vect Type k)
8using (k : Nat, ts : Vect Type k)
6 data HVect : Vect Type k -> Type where
9 data HVect : Vect Type k -> Type where
7 Nil : HVect []
10 Nil : HVect []
lib/Data/Vect.idr+3
@@ -2,6 +2,9 @@ module Data.Vect
2
2
3import Language.Reflection
3import Language.Reflection
4
4
5+%access public
6+%default total
7+
5--------------------------------------------------------------------------------
8--------------------------------------------------------------------------------
6-- Elem
9-- Elem
7--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------