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, PosT n) => Pos -> Pos -> Fin n
- type FinT i n = (i <=! n, PosT n)
- type FinWithMessageT msg i n = (LTEQT msg i n, PosT n)
- finC :: forall (i :: Nat) (n :: Nat). FinT i n => Fin n
- showFin :: Fin n -> String
- readFinP :: forall n. PosT n => ReadP (Fin n)
- readFin :: PosT n => ReadS (Fin n)
- mkFinC :: forall n. PosT n => Pos -> Pos -> Either String (Fin n)
- mkFin :: Pos -> Pos -> Either String (Fin n)
- fin :: PosT n => Int -> Either String (Fin n)
- finP :: forall n. PosT n => Pos -> Either String (Fin n)
- _F1 :: FinT 1 n => Fin n
- _F2 :: FinT 2 n => Fin n
- _F3 :: FinT 3 n => Fin n
- _F4 :: FinT 4 n => Fin n
- _F5 :: FinT 5 n => Fin n
- _F6 :: FinT 6 n => Fin n
- _F7 :: FinT 7 n => Fin n
- _F8 :: FinT 8 n => Fin n
- _F9 :: FinT 9 n => Fin n
- _F10 :: FinT 10 n => Fin n
- _F11 :: FinT 11 n => Fin n
- _F12 :: FinT 12 n => Fin n
- _F13 :: FinT 13 n => Fin n
- _F14 :: FinT 14 n => Fin n
- _F15 :: FinT 15 n => Fin n
- _F16 :: FinT 16 n => Fin n
- _F17 :: FinT 17 n => Fin n
- _F18 :: FinT 18 n => Fin n
- _F19 :: FinT 19 n => Fin n
- _F20 :: FinT 20 n => Fin n
Documentation
definition of the Finite type
Instances
pattern FinU :: forall (n :: Nat). (HasCallStack, PosT n) => Pos -> Pos -> Fin n Source #
pattern synonym for validating the fin before construction with a PosT constraint for validating at the typelevel
type FinWithMessageT msg i n = (LTEQT msg i n, PosT n) Source #
type constraint for restricting a Nat
to positive numbers with a custom error message
finC :: forall (i :: Nat) (n :: Nat). FinT i n => Fin n Source #
create a Fin
using typelevel "i" and "n" Nat
read/show methods
constructors
mkFinC :: forall n. PosT 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