| Copyright | (c) Grant Weyburne 2022 |
|---|---|
| License | BSD-3 |
| Safe Haskell | None |
| Language | Haskell2010 |
Cybus.Fin
Synopsis
- data Fin n
- fnPos :: Fin n -> Pos
- fnN :: Fin n -> Pos
- pattern Fin :: forall (n :: Nat). Pos -> Pos -> Fin n
- pattern FinU :: forall (n :: Nat). (HasCallStack, PosC n) => Pos -> Pos -> Fin n
- class (PosC i, PosC n) => FinC i n where
- class FinWithMessageC msg i n
- showFin :: Fin n -> String
- readFinP :: forall n. PosC n => ReadP (Fin n)
- readFin :: PosC n => ReadS (Fin n)
- mkFinC :: forall n. PosC n => Pos -> Pos -> Either String (Fin n)
- mkFin :: Pos -> Pos -> Either String (Fin n)
- fin :: PosC n => Int -> Either String (Fin n)
- finP :: forall n. PosC n => Pos -> Either String (Fin n)
- _F1 :: FinC 1 n => Fin n
- _F2 :: FinC 2 n => Fin n
- _F3 :: FinC 3 n => Fin n
- _F4 :: FinC 4 n => Fin n
- _F5 :: FinC 5 n => Fin n
- _F6 :: FinC 6 n => Fin n
- _F7 :: FinC 7 n => Fin n
- _F8 :: FinC 8 n => Fin n
- _F9 :: FinC 9 n => Fin n
- _F10 :: FinC 10 n => Fin n
- _F11 :: FinC 11 n => Fin n
- _F12 :: FinC 12 n => Fin n
- _F13 :: FinC 13 n => Fin n
- _F14 :: FinC 14 n => Fin n
- _F15 :: FinC 15 n => Fin n
- _F16 :: FinC 16 n => Fin n
- _F17 :: FinC 17 n => Fin n
- _F18 :: FinC 18 n => Fin n
- _F19 :: FinC 19 n => Fin n
- _F20 :: FinC 20 n => Fin n
Documentation
definition of the Finite type
Instances
pattern FinU :: forall (n :: Nat). (HasCallStack, PosC n) => Pos -> Pos -> Fin n Source #
pattern synonym for validating the fin before construction with a PosC constraint for validating at the typelevel
class (PosC i, PosC n) => FinC i n where Source #
class for constraining "i" to positive numbers less than or equal to "n"
class FinWithMessageC msg i n Source #
class for constraining "i" to positive numbers less than or equal to "n" with a custom error message
Instances
| LTEQT msg i n => FinWithMessageC msg i n Source # | |
Defined in Cybus.Fin | |
read/show methods
constructors
mkFinC :: forall n. PosC n => Pos -> Pos -> Either String (Fin n) Source #
create a Fin value level "i" and "n" values and validate against expected "n"
mkFin :: Pos -> Pos -> Either String (Fin n) Source #
create a Fin value level "i" and "n" values and validate that "i" is in range