Safe Haskell	Safe-Inferred
Language	Haskell2010

Torch.GraduallyTyped.Index.Class

Documentation

type family IndexOutOfBound (idx :: Nat) (dim :: Dim (Name Symbol) (Size Nat)) where ... Source #

Equations

IndexOutOfBound idx dim = TypeError ((("Out of bound index " <> idx) <> " for dimension ") <> dim)

type family InRangeImplF (idx :: Index Nat) (dim :: Dim (Name Symbol) (Size Nat)) :: Bool where ... Source #

Equations

InRangeImplF 'UncheckedIndex _ = 'True
InRangeImplF _ ('Dim _ 'UncheckedSize) = 'True
InRangeImplF ('Index idx) ('Dim _ ('Size index)) = CmpNat idx index == 'LT

type family InRangeCheckF (idx :: Index Nat) (dim :: Dim (Name Symbol) (Size Nat)) (ok :: Bool) :: Constraint where ... Source #

Equations

InRangeCheckF _ _ 'True = ()
InRangeCheckF ('Index idx) dim _ = IndexOutOfBound idx dim