{-# 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 (
type Fin,
fnPos,
fnN,
pattern Fin,
pattern FinU,
FinC (..),
FinWithMessageC,
showFin,
readFinP,
readFin,
mkFinC,
mkFin,
fin,
finP,
_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
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)
fnPos :: Fin n -> Pos
fnPos :: Fin n -> Pos
fnPos (Fin' Pos
i Pos
_) = Pos
i
fnN :: Fin n -> Pos
fnN :: Fin n -> Pos
fnN (Fin' Pos
_ Pos
n) = Pos
n
{-# 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 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
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
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"
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
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
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
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)
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)
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
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
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)
type FinWithMessageC :: GL.ErrorMessage -> Nat -> Nat -> Constraint
class FinWithMessageC msg i n
instance LTEQT msg i n => FinWithMessageC msg i n
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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
_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