{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{- |
Module      : Cybus.Fin
Description : finite numbers
Copyright   : (c) Grant Weyburne, 2022
License     : BSD-3

used for single indexes into a 'Cybus.Mat.Mat' or 'Cybus.FinMat.FinMat'
-}
module Cybus.Fin (
  type Fin,
  fnPos,
  fnN,
  pattern Fin,
  pattern FinU,
  FinT,
  FinWithMessageT,
  finC,

  -- * read/show methods
  showFin,
  readFinP,
  readFin,

  -- * constructors

  -- * miscellaneous
  mkFinC,
  mkFin,
  fin,
  finP,

  -- * fin indexes
  _F1,
  _F2,
  _F3,
  _F4,
  _F5,
  _F6,
  _F7,
  _F8,
  _F9,
  _F10,
  _F11,
  _F12,
  _F13,
  _F14,
  _F15,
  _F16,
  _F17,
  _F18,
  _F19,
  _F20,
) where

import Control.DeepSeq
import Control.Monad
import Cybus.NatHelper
import Data.Kind
import Data.Pos
import GHC.Enum
import GHC.Generics (Generic, Generic1)
import GHC.Read (readPrec)
import GHC.Stack
import qualified GHC.TypeLits as GL
import GHC.TypeNats (Nat)
import Primus.Enum
import Primus.Error
import Primus.Extra
import Primus.Num1
import qualified Text.ParserCombinators.ReadP as P
import qualified Text.ParserCombinators.ReadPrec as PC

-- | definition of the Finite type
type Fin :: Nat -> Type
data Fin n = Fin' !Pos !Pos
  deriving stock (Fin n -> Fin n -> Bool
(Fin n -> Fin n -> Bool) -> (Fin n -> Fin n -> Bool) -> Eq (Fin n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: Nat). Fin n -> Fin n -> Bool
/= :: Fin n -> Fin n -> Bool
$c/= :: forall (n :: Nat). Fin n -> Fin n -> Bool
== :: Fin n -> Fin n -> Bool
$c== :: forall (n :: Nat). Fin n -> Fin n -> Bool
Eq, Eq (Fin n)
Eq (Fin n)
-> (Fin n -> Fin n -> Ordering)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> Ord (Fin n)
Fin n -> Fin n -> Bool
Fin n -> Fin n -> Ordering
Fin n -> Fin n -> Fin n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (n :: Nat). Eq (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Bool
forall (n :: Nat). Fin n -> Fin n -> Ordering
forall (n :: Nat). Fin n -> Fin n -> Fin n
min :: Fin n -> Fin n -> Fin n
$cmin :: forall (n :: Nat). Fin n -> Fin n -> Fin n
max :: Fin n -> Fin n -> Fin n
$cmax :: forall (n :: Nat). Fin n -> Fin n -> Fin n
>= :: Fin n -> Fin n -> Bool
$c>= :: forall (n :: Nat). Fin n -> Fin n -> Bool
> :: Fin n -> Fin n -> Bool
$c> :: forall (n :: Nat). Fin n -> Fin n -> Bool
<= :: Fin n -> Fin n -> Bool
$c<= :: forall (n :: Nat). Fin n -> Fin n -> Bool
< :: Fin n -> Fin n -> Bool
$c< :: forall (n :: Nat). Fin n -> Fin n -> Bool
compare :: Fin n -> Fin n -> Ordering
$ccompare :: forall (n :: Nat). Fin n -> Fin n -> Ordering
$cp1Ord :: forall (n :: Nat). Eq (Fin n)
Ord, (forall x. Fin n -> Rep (Fin n) x)
-> (forall x. Rep (Fin n) x -> Fin n) -> Generic (Fin n)
forall x. Rep (Fin n) x -> Fin n
forall x. Fin n -> Rep (Fin n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (Fin n) x -> Fin n
forall (n :: Nat) x. Fin n -> Rep (Fin n) x
$cto :: forall (n :: Nat) x. Rep (Fin n) x -> Fin n
$cfrom :: forall (n :: Nat) x. Fin n -> Rep (Fin n) x
Generic, (forall (a :: Nat). Fin a -> Rep1 Fin a)
-> (forall (a :: Nat). Rep1 Fin a -> Fin a) -> Generic1 Fin
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall (a :: Nat). Rep1 Fin a -> Fin a
forall (a :: Nat). Fin a -> Rep1 Fin a
$cto1 :: forall (a :: Nat). Rep1 Fin a -> Fin a
$cfrom1 :: forall (a :: Nat). Fin a -> Rep1 Fin a
Generic1)
  deriving anyclass (Fin n -> ()
(Fin n -> ()) -> NFData (Fin n)
forall a. (a -> ()) -> NFData a
forall (n :: Nat). Fin n -> ()
rnf :: Fin n -> ()
$crnf :: forall (n :: Nat). Fin n -> ()
NFData)

-- | accessor for the index position within a 'Fin'
fnPos :: Fin n -> Pos
fnPos :: Fin n -> Pos
fnPos (Fin' Pos
i Pos
_) = Pos
i

-- | accessor for the maximum size within a 'Fin'
fnN :: Fin n -> Pos
fnN :: Fin n -> Pos
fnN (Fin' Pos
_ Pos
n) = Pos
n

-- | readonly pattern synonym for fin
{-# COMPLETE Fin #-}

pattern Fin ::
  forall (n :: Nat).
  Pos ->
  Pos ->
  Fin n
pattern $mFin :: forall r (n :: Nat).
Fin n -> (Pos -> Pos -> r) -> (Void# -> r) -> r
Fin i n <- Fin' i n

{-# COMPLETE FinU #-}

-- | pattern synonym for validating the fin before construction with a PosT constraint for validating at the typelevel
pattern FinU ::
  forall (n :: Nat).
  (HasCallStack, PosT n) =>
  Pos ->
  Pos ->
  Fin n
pattern $bFinU :: Pos -> Pos -> Fin n
$mFinU :: forall r (n :: Nat).
(HasCallStack, PosT n) =>
Fin n -> (Pos -> Pos -> r) -> (Void# -> r) -> r
FinU i n <-
  Fin' i n
  where
    FinU = Either String (Fin n) -> Fin n
forall a. HasCallStack => Either String a -> a
frp (Either String (Fin n) -> Fin n)
-> (Pos -> Pos -> Either String (Fin n)) -> Pos -> Pos -> Fin n
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ Pos -> Pos -> Either String (Fin n)
forall (n :: Nat). PosT n => Pos -> Pos -> Either String (Fin n)
mkFinC -- dont change this: frp is good else breaking the system

-- | create a 'Fin' value level "i" and "n" values and validate that "i" is in range
mkFin :: Pos -> Pos -> Either String (Fin n)
mkFin :: Pos -> Pos -> Either String (Fin n)
mkFin Pos
p Pos
n = String -> Either String (Fin n) -> Either String (Fin n)
forall a. String -> Either String a -> Either String a
lmsg String
"mkFin" (Either String (Fin n) -> Either String (Fin n))
-> Either String (Fin n) -> Either String (Fin n)
forall a b. (a -> b) -> a -> b
$ do
  if Pos
p Pos -> Pos -> Bool
forall a. Ord a => a -> a -> Bool
<= Pos
n
    then Fin n -> Either String (Fin n)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pos -> Pos -> Fin n
forall (n :: Nat). Pos -> Pos -> Fin n
Fin' Pos
p Pos
n)
    else String -> Either String (Fin n)
forall a b. a -> Either a b
Left (String -> Either String (Fin n))
-> String -> Either String (Fin n)
forall a b. (a -> b) -> a -> b
$ Pos -> String
forall a. Show a => a -> String
show Pos
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is too large: maximum is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pos -> String
forall a. Show a => a -> String
show Pos
n

-- | create a 'Fin' value level "i" and "n" values and validate against expected "n"
mkFinC :: forall n. PosT n => Pos -> Pos -> Either String (Fin n)
mkFinC :: Pos -> Pos -> Either String (Fin n)
mkFinC Pos
p Pos
n = do
  let n' :: Pos
n' = PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n
  if Pos
n Pos -> Pos -> Bool
forall a. Eq a => a -> a -> Bool
== Pos
n'
    then Pos -> Pos -> Either String (Fin n)
forall (n :: Nat). Pos -> Pos -> Either String (Fin n)
mkFin Pos
p Pos
n
    else String -> Either String (Fin n)
forall a b. a -> Either a b
Left (String -> Either String (Fin n))
-> String -> Either String (Fin n)
forall a b. (a -> b) -> a -> b
$ String
"mkFinC: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pos -> String
forall a. Show a => a -> String
show Pos
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" /= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pos -> String
forall a. Show a => a -> String
show Pos
n' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" at typelevel"

-- | convenience function for conversion from 'Int' to 'Fin'
fin :: PosT n => Int -> Either String (Fin n)
fin :: Int -> Either String (Fin n)
fin = Pos -> Either String (Fin n)
forall (n :: Nat). PosT n => Pos -> Either String (Fin n)
finP (Pos -> Either String (Fin n))
-> (Int -> Either String Pos) -> Int -> Either String (Fin n)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Int -> Either String Pos
eitherPos

-- | convenience function for conversion from 'Pos' to 'Fin'
finP :: forall n. PosT n => Pos -> Either String (Fin n)
finP :: Pos -> Either String (Fin n)
finP = (Pos -> Pos -> Either String (Fin n))
-> Pos -> Pos -> Either String (Fin n)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Pos -> Pos -> Either String (Fin n)
forall (n :: Nat). PosT n => Pos -> Pos -> Either String (Fin n)
mkFinC (PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n)

instance PosT n => Monoid (Fin n) where
  mempty :: Fin n
mempty = Fin n
forall a. Bounded a => a
minBound

instance Semigroup (Fin n) where
  <> :: Fin n -> Fin n -> Fin n
(<>) = Fin n -> Fin n -> Fin n
forall a. Ord a => a -> a -> a
max

-- PosT only needed for fromInteger
instance PosT n => Num (Fin n) where
  + :: Fin n -> Fin n -> Fin n
(+) = String -> Either String (Fin n) -> Fin n
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"(+)" (Either String (Fin n) -> Fin n)
-> (Fin n -> Fin n -> Either String (Fin n))
-> Fin n
-> Fin n
-> Fin n
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ (Integer -> Integer -> Integer)
-> Fin n -> Fin n -> Either String (Fin n)
forall a.
Num1 a =>
(Integer -> Integer -> Integer) -> a -> a -> Either String a
withOp2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
  (-) = String -> Either String (Fin n) -> Fin n
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"(-)" (Either String (Fin n) -> Fin n)
-> (Fin n -> Fin n -> Either String (Fin n))
-> Fin n
-> Fin n
-> Fin n
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ (Integer -> Integer -> Integer)
-> Fin n -> Fin n -> Either String (Fin n)
forall a.
Num1 a =>
(Integer -> Integer -> Integer) -> a -> a -> Either String a
withOp2 (-)
  * :: Fin n -> Fin n -> Fin n
(*) = String -> Either String (Fin n) -> Fin n
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"(*)" (Either String (Fin n) -> Fin n)
-> (Fin n -> Fin n -> Either String (Fin n))
-> Fin n
-> Fin n
-> Fin n
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.@ (Integer -> Integer -> Integer)
-> Fin n -> Fin n -> Either String (Fin n)
forall a.
Num1 a =>
(Integer -> Integer -> Integer) -> a -> a -> Either String a
withOp2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)
  abs :: Fin n -> Fin n
abs = Fin n -> Fin n
forall a. a -> a
id
  signum :: Fin n -> Fin n
signum (Fin Pos
_ Pos
n) = Pos -> Pos -> Fin n
forall (n :: Nat). (HasCallStack, PosT n) => Pos -> Pos -> Fin n
FinU Pos
_1P Pos
n
  negate :: Fin n -> Fin n
negate = String -> Fin n -> Fin n
forall a. HasCallStack => String -> a
normalError String
"Num (Fin n):negate is undefined"
  fromInteger :: Integer -> Fin n
fromInteger Integer
i = String -> Either String (Fin n) -> Fin n
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"Num (Fin n):fromInteger" (Either String (Fin n) -> Fin n) -> Either String (Fin n) -> Fin n
forall a b. (a -> b) -> a -> b
$ do
    Int
ii <- Integer -> Either String Int
integerToIntSafe (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
    Pos
k <- Int -> Either String Pos
eitherPos Int
ii
    Pos -> Pos -> Either String (Fin n)
forall (n :: Nat). PosT n => Pos -> Pos -> Either String (Fin n)
mkFinC Pos
k (PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n)

instance PosT n => Num1 (Fin n) where
  signum1 :: Either String (Fin n) -> Either String (Fin n)
signum1 = (Fin n -> Fin n) -> Either String (Fin n) -> Either String (Fin n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin n -> Fin n
forall a. Num a => a -> a
signum -- have to override as 1 is Fin 2 (there is no zero)

instance PosT n => Enum (Fin n) where
  toEnum :: Int -> Fin n
toEnum Int
i = String -> Either String (Fin n) -> Fin n
forall a. HasCallStack => String -> Either String a -> a
forceRight String
"Enum(Fin n):toEnum" (Either String (Fin n) -> Fin n) -> Either String (Fin n) -> Fin n
forall a b. (a -> b) -> a -> b
$ do
    Pos
p <- Int -> Either String Pos
eitherPos (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    Pos -> Pos -> Either String (Fin n)
forall (n :: Nat). PosT n => Pos -> Pos -> Either String (Fin n)
mkFinC Pos
p (PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n)
  fromEnum :: Fin n -> Int
fromEnum = Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1 (Int -> Int) -> (Fin n -> Int) -> Fin n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pos -> Int
unP (Pos -> Int) -> (Fin n -> Pos) -> Fin n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Pos
forall (n :: Nat). Fin n -> Pos
fnPos -- todo: ok subtract one could be a problem
  enumFrom :: Fin n -> [Fin n]
enumFrom = Fin n -> [Fin n]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
  enumFromThen :: Fin n -> Fin n -> [Fin n]
enumFromThen = Fin n -> Fin n -> [Fin n]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen

instance PosT n => Bounded (Fin n) where
  minBound :: Fin n
minBound = Pos -> Pos -> Fin n
forall (n :: Nat). (HasCallStack, PosT n) => Pos -> Pos -> Fin n
FinU Pos
_1P (PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n)
  maxBound :: Fin n
maxBound = Pos -> Pos -> Fin n
forall (n :: Nat). (HasCallStack, PosT n) => Pos -> Pos -> Fin n
FinU (PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n) (PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n)

-- | pretty print 'Fin'
showFin :: Fin n -> String
showFin :: Fin n -> String
showFin (Fin (Pos Int
i) (Pos Int
n)) = String
"Fin" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
i, Int
n)

instance PosT n => Read (Fin n) where
  readPrec :: ReadPrec (Fin n)
readPrec = (Int -> ReadP (Fin n)) -> ReadPrec (Fin n)
forall a. (Int -> ReadP a) -> ReadPrec a
PC.readP_to_Prec (ReadP (Fin n) -> Int -> ReadP (Fin n)
forall a b. a -> b -> a
const ReadP (Fin n)
forall (n :: Nat). PosT n => ReadP (Fin n)
readFinP)

-- | reader for 'Fin'
readFin :: PosT n => ReadS (Fin n)
readFin :: ReadS (Fin n)
readFin = ReadP (Fin n) -> ReadS (Fin n)
forall a. ReadP a -> ReadS a
P.readP_to_S ReadP (Fin n)
forall (n :: Nat). PosT n => ReadP (Fin n)
readFinP

-- | reader for 'showFin'
readFinP :: forall n. PosT n => P.ReadP (Fin n)
readFinP :: ReadP (Fin n)
readFinP = do
  ReadP ()
P.skipSpaces
  (Pos
i, Pos
n) <- ReadP String
-> ReadP String -> ReadP (Pos, Pos) -> ReadP (Pos, Pos)
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
P.between (String -> ReadP String
P.string String
"Fin(") (String -> ReadP String
P.string String
")") ((,) (Pos -> Pos -> (Pos, Pos))
-> ReadP Pos -> ReadP (Pos -> (Pos, Pos))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Pos
pPosInt ReadP (Pos -> (Pos, Pos))
-> ReadP Char -> ReadP (Pos -> (Pos, Pos))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> ReadP Char
P.char Char
',' ReadP (Pos -> (Pos, Pos)) -> ReadP Pos -> ReadP (Pos, Pos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadP Pos
pPosInt)
  (String -> ReadP (Fin n))
-> (Fin n -> ReadP (Fin n))
-> Either String (Fin n)
-> ReadP (Fin n)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ReadP (Fin n) -> String -> ReadP (Fin n)
forall a b. a -> b -> a
const ReadP (Fin n)
forall a. ReadP a
P.pfail) Fin n -> ReadP (Fin n)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pos -> Pos -> Either String (Fin n)
forall (n :: Nat). PosT n => Pos -> Pos -> Either String (Fin n)
mkFinC Pos
i Pos
n)

instance Show (Fin n) where
  show :: Fin n -> String
show = Fin n -> String
forall (n :: Nat). Fin n -> String
showFin

-- | create a 'Fin' using typelevel "i" and "n" Nat
finC :: forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC :: Fin n
finC = Pos -> Pos -> Fin n
forall (n :: Nat). Pos -> Pos -> Fin n
Fin' (PosT i => Pos
forall (n :: Nat). PosT n => Pos
fromNP @i) (PosT n => Pos
forall (n :: Nat). PosT n => Pos
fromNP @n)

-- | type constraint for restricting a 'Nat' to positive numbers
type FinT :: Nat -> Nat -> Constraint
type FinT i n = (i <=! n, PosT n)

-- | type constraint for restricting a 'Nat' to positive numbers with a custom error message
type FinWithMessageT :: GL.ErrorMessage -> Nat -> Nat -> Constraint
type FinWithMessageT msg i n = (LTEQT msg i n, PosT n)

-- | type synonym for index 1
_F1 :: FinT 1 n => Fin n
_F1 :: Fin n
_F1 = forall (n :: Nat). FinT 1 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @1

-- | type synonym for index 2
_F2 :: FinT 2 n => Fin n
_F2 :: Fin n
_F2 = forall (n :: Nat). FinT 2 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @2

-- | type synonym for index 3
_F3 :: FinT 3 n => Fin n
_F3 :: Fin n
_F3 = forall (n :: Nat). FinT 3 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @3

-- | type synonym for index 4
_F4 :: FinT 4 n => Fin n
_F4 :: Fin n
_F4 = forall (n :: Nat). FinT 4 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @4

-- | type synonym for index 5
_F5 :: FinT 5 n => Fin n
_F5 :: Fin n
_F5 = forall (n :: Nat). FinT 5 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @5

-- | type synonym for index 6
_F6 :: FinT 6 n => Fin n
_F6 :: Fin n
_F6 = forall (n :: Nat). FinT 6 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @6

-- | type synonym for index 7
_F7 :: FinT 7 n => Fin n
_F7 :: Fin n
_F7 = forall (n :: Nat). FinT 7 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @7

-- | type synonym for index 8
_F8 :: FinT 8 n => Fin n
_F8 :: Fin n
_F8 = forall (n :: Nat). FinT 8 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @8

-- | type synonym for index 9
_F9 :: FinT 9 n => Fin n
_F9 :: Fin n
_F9 = forall (n :: Nat). FinT 9 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @9

-- | type synonym for index 10
_F10 :: FinT 10 n => Fin n
_F10 :: Fin n
_F10 = forall (n :: Nat). FinT 10 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @10

-- | type synonym for index 11
_F11 :: FinT 11 n => Fin n
_F11 :: Fin n
_F11 = forall (n :: Nat). FinT 11 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @11

-- | type synonym for index 12
_F12 :: FinT 12 n => Fin n
_F12 :: Fin n
_F12 = forall (n :: Nat). FinT 12 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @12

-- | type synonym for index 13
_F13 :: FinT 13 n => Fin n
_F13 :: Fin n
_F13 = forall (n :: Nat). FinT 13 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @13

-- | type synonym for index 14
_F14 :: FinT 14 n => Fin n
_F14 :: Fin n
_F14 = forall (n :: Nat). FinT 14 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @14

-- | type synonym for index 15
_F15 :: FinT 15 n => Fin n
_F15 :: Fin n
_F15 = forall (n :: Nat). FinT 15 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @15

-- | type synonym for index 16
_F16 :: FinT 16 n => Fin n
_F16 :: Fin n
_F16 = forall (n :: Nat). FinT 16 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @16

-- | type synonym for index 17
_F17 :: FinT 17 n => Fin n
_F17 :: Fin n
_F17 = forall (n :: Nat). FinT 17 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @17

-- | type synonym for index 18
_F18 :: FinT 18 n => Fin n
_F18 :: Fin n
_F18 = forall (n :: Nat). FinT 18 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @18

-- | type synonym for index 19
_F19 :: FinT 19 n => Fin n
_F19 :: Fin n
_F19 = forall (n :: Nat). FinT 19 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @19

-- | type synonym for index 20
_F20 :: FinT 20 n => Fin n
_F20 :: Fin n
_F20 = forall (n :: Nat). FinT 20 n => Fin n
forall (i :: Nat) (n :: Nat). FinT i n => Fin n
finC @20