{-# 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,
  FinC (..),
  FinWithMessageC,

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

  -- * constructors
  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.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 PosC constraint for validating at the typelevel
pattern FinU ::
  forall (n :: Nat).
  (HasCallStack, PosC n) =>
  Pos ->
  Pos ->
  Fin n
pattern $bFinU :: Pos -> Pos -> Fin n
$mFinU :: forall r (n :: Nat).
(HasCallStack, PosC 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). PosC n => Pos -> Pos -> Either String (Fin n)
mkFinC

-- | 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. PosC n => Pos -> Pos -> Either String (Fin n)
mkFinC :: Pos -> Pos -> Either String (Fin n)
mkFinC Pos
p Pos
n = do
  let n' :: Pos
n' = PosC n => Pos
forall (n :: Nat). PosC 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 :: PosC n => Int -> Either String (Fin n)
fin :: Int -> Either String (Fin n)
fin = Pos -> Either String (Fin n)
forall (n :: Nat). PosC 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. PosC 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). PosC n => Pos -> Pos -> Either String (Fin n)
mkFinC (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n)

instance PosC 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

-- PosC only needed for fromInteger
instance PosC 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, PosC 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). PosC n => Pos -> Pos -> Either String (Fin n)
mkFinC Pos
k (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n)

instance PosC 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 PosC 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). PosC n => Pos -> Pos -> Either String (Fin n)
mkFinC Pos
p (PosC n => Pos
forall (n :: Nat). PosC 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
  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 PosC n => Bounded (Fin n) where
  minBound :: Fin n
minBound = Pos -> Pos -> Fin n
forall (n :: Nat). (HasCallStack, PosC n) => Pos -> Pos -> Fin n
FinU Pos
_1P (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n)
  maxBound :: Fin n
maxBound = Pos -> Pos -> Fin n
forall (n :: Nat). (HasCallStack, PosC n) => Pos -> Pos -> Fin n
FinU (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n) (PosC n => Pos
forall (n :: Nat). PosC 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 PosC 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). PosC n => ReadP (Fin n)
readFinP)

-- | reader for 'Fin'
readFin :: PosC 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). PosC n => ReadP (Fin n)
readFinP

-- | reader for 'showFin'
readFinP :: forall n. PosC 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). PosC 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

-- | class for constraining "i" to positive numbers less than or equal to "n"
type FinC :: Nat -> Nat -> Constraint
class (PosC i, PosC n) => FinC i n where
  finC :: Fin n

instance (PosC n, i <=! n) => FinC i n where
  finC :: Fin n
finC = Pos -> Pos -> Fin n
forall (n :: Nat). Pos -> Pos -> Fin n
Fin' (PosC i => Pos
forall (n :: Nat). PosC n => Pos
fromNP @i) (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n)

-- | class for constraining "i" to positive numbers less than or equal to "n" with a custom error message
type FinWithMessageC :: GL.ErrorMessage -> Nat -> Nat -> Constraint
class FinWithMessageC msg i n

instance LTEQT msg i n => FinWithMessageC msg i n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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