diff options
Diffstat (limited to 'src/Data/Array/Nested/Ranked')
| -rw-r--r-- | src/Data/Array/Nested/Ranked/Shape.hs | 8 | 
1 files changed, 8 insertions, 0 deletions
| diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs index 326bf61..3edebf6 100644 --- a/src/Data/Array/Nested/Ranked/Shape.hs +++ b/src/Data/Array/Nested/Ranked/Shape.hs @@ -43,6 +43,8 @@ import Data.Array.Nested.Lemmas  import Data.Array.Nested.Types +-- * Ranked lists +  type role ListR nominal representational  type ListR :: Nat -> Type -> Type  data ListR n i where @@ -171,6 +173,8 @@ listrPermutePrefix = \perm sh ->            GTI -> error "listrPermutePrefix: Index in permutation out of range" +-- * Ranked indices +  -- | An index into a rank-typed array.  type role IxR nominal representational  type IxR :: Nat -> Type -> Type @@ -191,6 +195,8 @@ infixr 3 :.:  {-# COMPLETE ZIR, (:.:) #-} +-- For convenience, this contains regular 'Int's instead of bounded integers +-- (traditionally called \"@Fin@\").  type IIxR n = IxR n Int  #ifdef OXAR_DEFAULT_SHOW_INSTANCES @@ -237,6 +243,8 @@ ixrPermutePrefix :: forall n i. [Int] -> IxR n i -> IxR n i  ixrPermutePrefix = coerce (listrPermutePrefix @i) +-- * Ranked shapes +  type role ShR nominal representational  type ShR :: Nat -> Type -> Type  newtype ShR n i = ShR (ListR n i) | 
