Safe Haskell	None
Language	GHC2021

Data.Fin

Contents

Orphan instances

Description

This file re-exports definitions from fin's Data.Fin, while adding a few more that are relevant to this context. Like Data.Fin, it is meant to be used qualified.

import Fin (Fin (..))
import qualified Fin as Fin

Synopsis

data Nat
- = Z
- | S Nat
data SNat (n :: Nat) where
- SZ :: SNat 'Z
- SS :: forall (n1 :: Nat). SNatI n1 => SNat ('S n1)
- pattern SS' :: forall m n. () => m ~ 'S n => SNat n -> SNat m
data Fin (n :: Nat) where
- FZ :: forall (n1 :: Nat). Fin ('S n1)
- FS :: forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
toNat :: forall (n :: Nat). Fin n -> Nat
fromNat :: forall (n :: Nat). SNatI n => Nat -> Maybe (Fin n)
toInteger :: Integral a => a -> Integer
mirror :: forall (n :: Nat). SNatI n => Fin n -> Fin n
absurd :: Fin Nat0 -> b
universe :: forall (n :: Nat). SNatI n => [Fin n]
f0 :: forall (n :: Nat). Fin ('S n)
f1 :: forall (n :: Nat). Fin ('S ('S n))
f2 :: forall (n :: Nat). Fin ('S ('S ('S n)))
f3 :: forall (n :: Nat). Fin ('S ('S ('S ('S n))))
invert :: forall (n :: Nat). SNatI n => Fin n -> Fin n
shiftN :: forall (n :: Nat) (m :: Nat). SNat n -> Fin m -> Fin (n + m)
shift1 :: forall (m :: Nat). Fin m -> Fin ('S m)
weakenFin :: forall proxy (m :: Nat) (n :: Nat). proxy m -> Fin n -> Fin (m + n)
weakenFinRight :: forall proxy (m :: Nat) (n :: Nat). proxy m -> Fin n -> Fin (n + m)
weaken1Fin :: forall (n :: Nat). Fin n -> Fin ('S n)
weaken1FinRight :: forall (n :: Nat). Fin n -> Fin (n + N1)
strengthen1Fin :: forall (n :: Nat). SNatI n => Fin ('S n) -> Maybe (Fin n)
strengthenRecFin :: forall (k :: Nat) (m :: Nat) proxy (n :: Nat). SNat k -> SNat m -> proxy n -> Fin (k + (m + n)) -> Maybe (Fin (k + n))

Documentation

data Nat #

Nat natural numbers.

Better than GHC's built-in Nat for some use cases.

Constructors

Z
S Nat

Instances

Instances details

Arbitrary Nat

Instance details

Defined in Data.Nat

Methods

arbitrary :: Gen Nat #

shrink :: Nat -> [Nat] #

CoArbitrary Nat

Instance details

Defined in Data.Nat

Methods

coarbitrary :: Nat -> Gen b -> Gen b #

Function Nat

Instance details

Defined in Data.Nat

Methods

function :: (Nat -> b) -> Nat :-> b #

Data Nat

Instance details

Defined in Data.Nat

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat #

toConstr :: Nat -> Constr #

dataTypeOf :: Nat -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Nat) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat) #

gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #

gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #

Enum Nat

Instance details

Defined in Data.Nat

Methods

succ :: Nat -> Nat #

pred :: Nat -> Nat #

toEnum :: Int -> Nat #

fromEnum :: Nat -> Int #

enumFrom :: Nat -> [Nat] #

enumFromThen :: Nat -> Nat -> [Nat] #

enumFromTo :: Nat -> Nat -> [Nat] #

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #

Num Nat

Instance details

Defined in Data.Nat

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Integral Nat

Instance details

Defined in Data.Nat

Methods

quot :: Nat -> Nat -> Nat #

rem :: Nat -> Nat -> Nat #

div :: Nat -> Nat -> Nat #

mod :: Nat -> Nat -> Nat #

quotRem :: Nat -> Nat -> (Nat, Nat) #

divMod :: Nat -> Nat -> (Nat, Nat) #

toInteger :: Nat -> Integer #

Real Nat

Instance details

Defined in Data.Nat

Methods

toRational :: Nat -> Rational #

Show Nat

Nat is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Instance details

Defined in Data.Nat

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

NFData Nat

Instance details

Defined in Data.Nat

Methods

rnf :: Nat -> () #

Eq Nat

Instance details

Defined in Data.Nat

Methods

(==) :: Nat -> Nat -> Bool #

(/=) :: Nat -> Nat -> Bool #

Ord Nat

Instance details

Defined in Data.Nat

Methods

compare :: Nat -> Nat -> Ordering #

(<) :: Nat -> Nat -> Bool #

(<=) :: Nat -> Nat -> Bool #

(>) :: Nat -> Nat -> Bool #

(>=) :: Nat -> Nat -> Bool #

max :: Nat -> Nat -> Nat #

min :: Nat -> Nat -> Nat #

Hashable Nat

Instance details

Defined in Data.Nat

Methods

hashWithSalt :: Int -> Nat -> Int #

hash :: Nat -> Int #

Universe Nat

>>> import qualified Data.Universe.Class as U
>>> take 10 (U.universe :: [Nat])
[0,1,2,3,4,5,6,7,8,9]

Since: fin-0.1.2

Instance details

Defined in Data.Nat

Methods

universe :: [Nat] #

Category LEProof

The other variant (LEPRoof) isn't Category, because leRefl requires SNat evidence.

Instance details

Defined in Data.Type.Nat.LE.ReflStep

Methods

id :: forall (a :: Nat). LEProof a a #

(.) :: forall (b :: Nat) (c :: Nat) (a :: Nat). LEProof b c -> LEProof a b -> LEProof a c #

TestEquality SNat

Instance details

Defined in Data.Type.Nat

Methods

testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #

TestEquality PatN Source #

Instance details

Defined in Rebound.Bind.PatN

Methods

testEquality :: forall (a :: Nat) (b :: Nat). PatN a -> PatN b -> Maybe (a :~: b) #

EqP Fin

>>> eqp FZ FZ
True

>>> eqp FZ (FS FZ)
False

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
[True,False,False,False,False,False]
[False,True,False,False,False,False]
[False,False,True,False,False,False]
[False,False,False,True,False,False]

Since: fin-0.2.2

Instance details

Defined in Data.Fin

Methods

eqp :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Bool #

EqP SNat

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

eqp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Bool #

GNFData SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

grnf :: forall (a :: Nat). SNat a -> () #

GCompare SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gcompare :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> GOrdering a b #

GEq SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

geq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #

GShow Fin

Since: fin-0.2.2

Instance details

Defined in Data.Fin

Methods

gshowsPrec :: forall (a :: Nat). Int -> Fin a -> ShowS #

GShow SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gshowsPrec :: forall (a :: Nat). Int -> SNat a -> ShowS #

OrdP Fin

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
[EQ,LT,LT,LT,LT,LT]
[GT,EQ,LT,LT,LT,LT]
[GT,GT,EQ,LT,LT,LT]
[GT,GT,GT,EQ,LT,LT]

Since: fin-0.2.2

Instance details

Defined in Data.Fin

Methods

comparep :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Ordering #

OrdP SNat

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

comparep :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Ordering #

GSubst b (V1 :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gsubst :: forall (m :: Nat) (n :: Nat). Env b m n -> V1 m -> V1 n Source #

GSubst v (U1 :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gsubst :: forall (m :: Nat) (n :: Nat). Env v m n -> U1 m -> U1 n Source #

Generic1 (List a :: Nat -> Type) Source #

Enable generic programming for the List type We can't derive the Generic1 instance for List using newtype deriving because the kinds differ. Therefore we need to write it by hand.

Instance details

Defined in Data.Scoped.List

Associated Types

type Rep1 (List a :: Nat -> Type)
Instance details Defined in Data.Scoped.List type Rep1 (List a :: Nat -> Type) = (U1 :: Nat -> Type) :+: (Rec1 a :*: Rec1 (List a))

Methods

from1 :: forall (a0 :: Nat). List a a0 -> Rep1 (List a) a0 #

to1 :: forall (a0 :: Nat). Rep1 (List a) a0 -> List a a0 #

Generic1 (Maybe a :: Nat -> Type) Source #

Instance details

Defined in Data.Scoped.Maybe

Associated Types

type Rep1 (Maybe a :: Nat -> Type)
Instance details Defined in Data.Scoped.Maybe type Rep1 (Maybe a :: Nat -> Type) = (U1 :: Nat -> Type) :+: Rec1 a

Methods

from1 :: forall (a0 :: Nat). Maybe a a0 -> Rep1 (Maybe a) a0 #

to1 :: forall (a0 :: Nat). Rep1 (Maybe a) a0 -> Maybe a a0 #

Subst b g => GSubst b (Rec1 g) Source #

Instance details

Defined in Rebound.Generics

Methods

gsubst :: forall (m :: Nat) (n :: Nat). Env b m n -> Rec1 g m -> Rec1 g n Source #

Subst v t => Subst v (List t) Source #

Instance details

Defined in Rebound.Env

Methods

applyE :: forall (n :: Nat) (m :: Nat). Env v n m -> List t n -> List t m Source #

isVar :: forall (n :: Nat). List t n -> Maybe (v :~: List t, Fin n) Source #

(GSubst b f, GSubst b g) => GSubst b (f :*: g) Source #

Instance details

Defined in Rebound.Generics

Methods

gsubst :: forall (m :: Nat) (n :: Nat). Env b m n -> (f :*: g) m -> (f :*: g) n Source #

(GSubst b f, GSubst b g) => GSubst b (f :+: g) Source #

Instance details

Defined in Rebound.Generics

Methods

gsubst :: forall (m :: Nat) (n :: Nat). Env b m n -> (f :+: g) m -> (f :+: g) n Source #

GSubst v (K1 i c :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gsubst :: forall (m :: Nat) (n :: Nat). Env v m n -> K1 i c m -> K1 i c n Source #

GSubst b f => GSubst b (M1 i c f) Source #

Instance details

Defined in Rebound.Generics

Methods

gsubst :: forall (m :: Nat) (n :: Nat). Env b m n -> M1 i c f m -> M1 i c f n Source #

GFV (U1 :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gappearsFree :: forall (n :: Nat). Fin n -> U1 n -> Bool Source #

gfreeVars :: forall (n :: Nat). U1 n -> Set (Fin n) Source #

GFV (V1 :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gappearsFree :: forall (n :: Nat). Fin n -> V1 n -> Bool Source #

gfreeVars :: forall (n :: Nat). V1 n -> Set (Fin n) Source #

GStrengthen (U1 :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gstrengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> U1 (k + (m + n)) -> Maybe (U1 (k + n)) Source #

GStrengthen (V1 :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gstrengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> V1 (k + (m + n)) -> Maybe (V1 (k + n)) Source #

FV t => FV (List t) Source #

Instance details

Defined in Rebound.Classes

Methods

appearsFree :: forall (n :: Nat). Fin n -> List t n -> Bool Source #

freeVars :: forall (n :: Nat). List t n -> Set (Fin n) Source #

FV t => GFV (Rec1 t) Source #

Instance details

Defined in Rebound.Generics

Methods

gappearsFree :: forall (n :: Nat). Fin n -> Rec1 t n -> Bool Source #

gfreeVars :: forall (n :: Nat). Rec1 t n -> Set (Fin n) Source #

Strengthen t => GStrengthen (Rec1 t) Source #

Instance details

Defined in Rebound.Generics

Methods

gstrengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> Rec1 t (k + (m + n)) -> Maybe (Rec1 t (k + n)) Source #

Strengthen t => Strengthen (List t) Source #

Instance details

Defined in Rebound.Classes

Methods

strengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> List t (k + (m + n)) -> Maybe (List t (k + n)) Source #

strengthenOneRec :: forall (k :: Nat) (n :: Nat). SNat k -> SNat n -> List t (k + 'S n) -> Maybe (List t (k + n)) Source #

(GFV f, GFV g) => GFV (f :*: g) Source #

Instance details

Defined in Rebound.Generics

Methods

gappearsFree :: forall (n :: Nat). Fin n -> (f :*: g) n -> Bool Source #

gfreeVars :: forall (n :: Nat). (f :*: g) n -> Set (Fin n) Source #

(GFV f, GFV g) => GFV (f :+: g) Source #

Instance details

Defined in Rebound.Generics

Methods

gappearsFree :: forall (n :: Nat). Fin n -> (f :+: g) n -> Bool Source #

gfreeVars :: forall (n :: Nat). (f :+: g) n -> Set (Fin n) Source #

GFV (K1 i c :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gappearsFree :: forall (n :: Nat). Fin n -> K1 i c n -> Bool Source #

gfreeVars :: forall (n :: Nat). K1 i c n -> Set (Fin n) Source #

(GStrengthen f, GStrengthen g) => GStrengthen (f :*: g) Source #

Instance details

Defined in Rebound.Generics

Methods

gstrengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> (f :*: g) (k + (m + n)) -> Maybe ((f :*: g) (k + n)) Source #

(GStrengthen f, GStrengthen g) => GStrengthen (f :+: g) Source #

Instance details

Defined in Rebound.Generics

Methods

gstrengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> (f :+: g) (k + (m + n)) -> Maybe ((f :+: g) (k + n)) Source #

GStrengthen (K1 i c :: Nat -> Type) Source #

Instance details

Defined in Rebound.Generics

Methods

gstrengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> K1 i c (k + (m + n)) -> Maybe (K1 i c (k + n)) Source #

GFV f => GFV (M1 i c f) Source #

Instance details

Defined in Rebound.Generics

Methods

gappearsFree :: forall (n :: Nat). Fin n -> M1 i c f n -> Bool Source #

gfreeVars :: forall (n :: Nat). M1 i c f n -> Set (Fin n) Source #

GStrengthen f => GStrengthen (M1 i c f) Source #

Instance details

Defined in Rebound.Generics

Methods

gstrengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> M1 i c f (k + (m + n)) -> Maybe (M1 i c f (k + n)) Source #

type Rep1 (List a :: Nat -> Type) Source #

Instance details

Defined in Data.Scoped.List

type Rep1 (List a :: Nat -> Type) = (U1 :: Nat -> Type) :+: (Rec1 a :*: Rec1 (List a))

type Rep1 (Maybe a :: Nat -> Type) Source #

Instance details

Defined in Data.Scoped.Maybe

type Rep1 (Maybe a :: Nat -> Type) = (U1 :: Nat -> Type) :+: Rec1 a

data SNat (n :: Nat) where #

Singleton of Nat.

Constructors

SZ :: SNat 'Z
SS :: forall (n1 :: Nat). SNatI n1 => SNat ('S n1)

Bundled Patterns

pattern SS' :: forall m n. () => m ~ 'S n => SNat n -> SNat m

A pattern with explicit argument

>>> let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = n
>>> predSNat (SS' (SS' SZ))
SS

>>> reflect $ predSNat (SS' (SS' SZ))
1

Since: fin-0.3.2

Instances

Instances details

TestEquality SNat

Instance details

Defined in Data.Type.Nat

Methods

testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #

EqP SNat

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

eqp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Bool #

GNFData SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

grnf :: forall (a :: Nat). SNat a -> () #

GCompare SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gcompare :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> GOrdering a b #

GEq SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

geq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #

GShow SNat

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gshowsPrec :: forall (a :: Nat). Int -> SNat a -> ShowS #

OrdP SNat

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

comparep :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Ordering #

SNatI n => Arbitrary (SNat n) Source #

Instance details

Defined in Data.SNat

Methods

arbitrary :: Gen (SNat n) #

shrink :: SNat n -> [SNat n] #

Show (SNat p)

Instance details

Defined in Data.Type.Nat

Methods

showsPrec :: Int -> SNat p -> ShowS #

show :: SNat p -> String #

showList :: [SNat p] -> ShowS #

SNatI n => Boring (SNat n)

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

boring :: SNat n #

NFData (SNat n)

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

rnf :: SNat n -> () #

Eq (SNat a)

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

(==) :: SNat a -> SNat a -> Bool #

(/=) :: SNat a -> SNat a -> Bool #

Ord (SNat a)

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

compare :: SNat a -> SNat a -> Ordering #

(<) :: SNat a -> SNat a -> Bool #

(<=) :: SNat a -> SNat a -> Bool #

(>) :: SNat a -> SNat a -> Bool #

(>=) :: SNat a -> SNat a -> Bool #

max :: SNat a -> SNat a -> SNat a #

min :: SNat a -> SNat a -> SNat a #

ToInt (SNat n) Source #

Instance details

Defined in Data.SNat

Methods

toInt :: SNat n -> Int Source #

Sized (SNat n) Source #

Instance details

Defined in Rebound.Classes

Associated Types

type Size (SNat n)
Instance details Defined in Rebound.Classes type Size (SNat n) = n

Methods

size :: SNat n -> SNat (Size (SNat n)) Source #

PatEq (SNat n1) (SNat n2) Source #

Instance details

Defined in Rebound.Classes

Methods

patEq :: SNat n1 -> SNat n2 -> Maybe (Size (SNat n1) :~: Size (SNat n2)) Source #

type Size (SNat n) Source #

Instance details

Defined in Rebound.Classes

type Size (SNat n) = n

data Fin (n :: Nat) where #

Finite numbers: [0..n-1].

Constructors

FZ :: forall (n1 :: Nat). Fin ('S n1)
FS :: forall (n1 :: Nat). Fin n1 -> Fin ('S n1)

Instances

Instances details

FV Fin Source #
Instance details Defined in Rebound.Classes Methods appearsFree :: forall (n :: Nat). Fin n -> Fin n -> Bool Source # freeVars :: forall (n :: Nat). Fin n -> Set (Fin n) Source #
Shiftable Fin Source #
Instance details Defined in Rebound.Env Methods shift :: forall (k :: Nat) (n :: Nat). SNat k -> Fin n -> Fin (k + n) Source #
Strengthen Fin Source #
Instance details Defined in Rebound.Classes Methods strengthenRec :: forall (k :: Nat) (m :: Nat) (n :: Nat). SNat k -> SNat m -> SNat n -> Fin (k + (m + n)) -> Maybe (Fin (k + n)) Source # strengthenOneRec :: forall (k :: Nat) (n :: Nat). SNat k -> SNat n -> Fin (k + 'S n) -> Maybe (Fin (k + n)) Source #
SubstVar Fin Source #
Instance details Defined in Rebound.Env Methods var :: forall (n :: Nat). Fin n -> Fin n Source #
GSubst b Fin Source #
Instance details Defined in Rebound.Env Methods gsubst :: forall (m :: Nat) (n :: Nat). Env b m n -> Fin m -> Fin n Source #
Subst Fin Fin Source #
Instance details Defined in Rebound.Env Methods applyE :: forall (n :: Nat) (m :: Nat). Env Fin n m -> Fin n -> Fin m Source # isVar :: forall (n :: Nat). Fin n -> Maybe (Fin :~: Fin, Fin n) Source #
SubstVar v => Subst v Fin Source #
Instance details Defined in Rebound.Env Methods applyE :: forall (n :: Nat) (m :: Nat). Env v n m -> Fin n -> Fin m Source # isVar :: forall (n :: Nat). Fin n -> Maybe (v :~: Fin, Fin n) Source #
EqP Fin	`>>>` `eqp FZ FZ`True `>>>` `eqp FZ (FS FZ)`False `>>>` `let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y \| y <- ys ] \| x <- xs ]`[True,False,False,False,False,False] [False,True,False,False,False,False] [False,False,True,False,False,False] [False,False,False,True,False,False] Since: fin-0.2.2
Instance details Defined in Data.Fin Methods eqp :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Bool #
GShow Fin	Since: fin-0.2.2
Instance details Defined in Data.Fin Methods gshowsPrec :: forall (a :: Nat). Int -> Fin a -> ShowS #
OrdP Fin	`>>>` `let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y \| y <- ys ] \| x <- xs ]`[EQ,LT,LT,LT,LT,LT] [GT,EQ,LT,LT,LT,LT] [GT,GT,EQ,LT,LT,LT] [GT,GT,GT,EQ,LT,LT] Since: fin-0.2.2
Instance details Defined in Data.Fin Methods comparep :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Ordering #
(n ~ 'S m, SNatI m) => Arbitrary (Fin n)
Instance details Defined in Data.Fin Methods arbitrary :: Gen (Fin n) # shrink :: Fin n -> [Fin n] #
CoArbitrary (Fin n)
Instance details Defined in Data.Fin Methods coarbitrary :: Fin n -> Gen b -> Gen b #
(n ~ 'S m, SNatI m) => Function (Fin n)
Instance details Defined in Data.Fin Methods function :: (Fin n -> b) -> Fin n :-> b #
(n ~ 'S m, SNatI m) => Bounded (Fin n)
Instance details Defined in Data.Fin Methods minBound :: Fin n # maxBound :: Fin n #
SNatI n => Enum (Fin n)
Instance details Defined in Data.Fin Methods succ :: Fin n -> Fin n # pred :: Fin n -> Fin n # toEnum :: Int -> Fin n # fromEnum :: Fin n -> Int # enumFrom :: Fin n -> [Fin n] # enumFromThen :: Fin n -> Fin n -> [Fin n] # enumFromTo :: Fin n -> Fin n -> [Fin n] # enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n] #
SNatI n => Num (Fin n)	Operations module `n`. `>>>` `map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]`[0,1,2,0,1,1] `>>>` `fromInteger 42 :: Fin N.Nat0`* Exception: divide by zero ... `>>>` `signum (FZ :: Fin N.Nat1)`0 `>>>` `signum (3 :: Fin N.Nat4)`1 `>>>` `2 + 3 :: Fin N.Nat4`1 `>>>` `2 * 3 :: Fin N.Nat4`**2
Instance details Defined in Data.Fin Methods (+) :: Fin n -> Fin n -> Fin n # (-) :: Fin n -> Fin n -> Fin n # (*) :: Fin n -> Fin n -> Fin n # negate :: Fin n -> Fin n # abs :: Fin n -> Fin n # signum :: Fin n -> Fin n # fromInteger :: Integer -> Fin n #
SNatI n => Integral (Fin n)	`quot` works only on `Fin n` where `n` is prime.
Instance details Defined in Data.Fin Methods quot :: Fin n -> Fin n -> Fin n # rem :: Fin n -> Fin n -> Fin n # div :: Fin n -> Fin n -> Fin n # mod :: Fin n -> Fin n -> Fin n # quotRem :: Fin n -> Fin n -> (Fin n, Fin n) # divMod :: Fin n -> Fin n -> (Fin n, Fin n) # toInteger :: Fin n -> Integer #
SNatI n => Real (Fin n)
Instance details Defined in Data.Fin Methods toRational :: Fin n -> Rational #
Show (Fin n)	`Fin` is printed as `Natural`. To see explicit structure, use `explicitShow` or `explicitShowsPrec`
Instance details Defined in Data.Fin Methods showsPrec :: Int -> Fin n -> ShowS # show :: Fin n -> String # showList :: [Fin n] -> ShowS #
n ~ 'Z => Absurd (Fin n)	Since: fin-0.2.1
Instance details Defined in Data.Fin Methods absurd :: Fin n -> b #
NFData (Fin n)
Instance details Defined in Data.Fin Methods rnf :: Fin n -> () #
Eq (Fin n)
Instance details Defined in Data.Fin Methods (==) :: Fin n -> Fin n -> Bool # (/=) :: Fin n -> Fin n -> Bool #
Ord (Fin n)
Instance details Defined in Data.Fin Methods compare :: 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 # max :: Fin n -> Fin n -> Fin n # min :: Fin n -> Fin n -> Fin n #
Hashable (Fin n)
Instance details Defined in Data.Fin Methods hashWithSalt :: Int -> Fin n -> Int # hash :: Fin n -> Int #
ToInt (Fin n) Source #	The `toInteger` instance for Fin has an unnecessary type class constraint (NatI n) for Fin. So we also include this class for simple conversion.
Instance details Defined in Data.Fin Methods toInt :: Fin n -> Int Source #
SNatI n => Finite (Fin n)	`>>>` `(U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))`True Since: fin-0.1.2
Instance details Defined in Data.Fin Methods universeF :: [Fin n] # cardinality :: Tagged (Fin n) Natural #
SNatI n => Universe (Fin n)	Since: fin-0.1.2
Instance details Defined in Data.Fin Methods universe :: [Fin n] #
SNatI n => FoldableWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m # ifoldMap' :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m # ifoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b # ifoldl :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b # ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b # ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b #
FoldableWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.Lazy Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m # ifoldMap' :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m # ifoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b # ifoldl :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b # ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b # ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b #
SNatI n => FoldableWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.Pull Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m # ifoldMap' :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m # ifoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b # ifoldl :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b # ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b # ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b #
SNatI n => FunctorWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b #
FunctorWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.Lazy Methods imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b #
FunctorWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.Pull Methods imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b #
SNatI n => TraversableWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) #
TraversableWithIndex (Fin n) (Vec n)	Since: vec-0.4
Instance details Defined in Data.Vec.Lazy Methods itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) #

toNat :: forall (n :: Nat). Fin n -> Nat #

Convert to Nat.

fromNat :: forall (n :: Nat). SNatI n => Nat -> Maybe (Fin n) #

Convert from Nat.

>>> fromNat N.nat1 :: Maybe (Fin N.Nat2)
Just 1

>>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
Nothing

toInteger :: Integral a => a -> Integer #

conversion to Integer

mirror :: forall (n :: Nat). SNatI n => Fin n -> Fin n #

Mirror the values, minBound becomes maxBound, etc.

>>> map mirror universe :: [Fin N.Nat4]
[3,2,1,0]

>>> reverse universe :: [Fin N.Nat4]
[3,2,1,0]

Since: fin-0.1.1

absurd :: Fin Nat0 -> b #

Fin Nat0 is not inhabited.

universe :: forall (n :: Nat). SNatI n => [Fin n] #

All values. [minBound .. maxBound] won't work for Fin Nat0.

>>> universe :: [Fin N.Nat3]
[0,1,2]

f0 :: forall (n :: Nat). Fin ('S n) Source #

f1 :: forall (n :: Nat). Fin ('S ('S n)) Source #

f2 :: forall (n :: Nat). Fin ('S ('S ('S n))) Source #

f3 :: forall (n :: Nat). Fin ('S ('S ('S ('S n)))) Source #

invert :: forall (n :: Nat). SNatI n => Fin n -> Fin n Source #

List all numbers up to some size >>> universe :: [Fin N3] [0,1,2]

Convert an "index" Fin to a "level" Fin and vice versa.

shiftN :: forall (n :: Nat) (m :: Nat). SNat n -> Fin m -> Fin (n + m) Source #

Increment by a fixed amount (on the left).

shift1 :: forall (m :: Nat). Fin m -> Fin ('S m) Source #

Increment by one.

weakenFin :: forall proxy (m :: Nat) (n :: Nat). proxy m -> Fin n -> Fin (m + n) Source #

Weaken the bound of a Fin by an arbitrary amount, without changing its index.

Weakenening changes the bound of a nat-indexed type without changing its value. These operations can either be defined for the n-ary case (as in Fin below) or be defined in terms of a single-step operation. However, as both of these operations are identity functions, it is justified to use unsafeCoerce.

The corresponding function in the Data.Fin library is weakenLeft.

-- >>> :t weakenLeft
weakenLeft :: SNatI n => Proxy m -> Fin n -> Fin (Plus n m)

This function does not change the value, it only changes its type.

-- >>> weakenLeft (Proxy :: Proxy N1) (f1 :: Fin N2) :: Fin N3
1

We could use the following definition:

weakenFin m f = withSNat m $ weakenLeft (Proxy :: Proxy m) f

But, by using an unsafeCoerce implementation, we can avoid the SNatI n constraint in the type of this operation.

-- >>> weakenFin (Proxy :: Proxy N1) (f1 :: Fin N2) :: Fin N3
1

weakenFinRight :: forall proxy (m :: Nat) (n :: Nat). proxy m -> Fin n -> Fin (n + m) Source #

Weaken the bound of of a Fin by an arbitrary amount on the right. This is also an identity function >>> weakenFinRight (s1 :: SNat N1) (f1 :: Fin N2) :: Fin N3 1

weaken1Fin :: forall (n :: Nat). Fin n -> Fin ('S n) Source #

Weaken the bound of a Fin by 1.

weaken1FinRight :: forall (n :: Nat). Fin n -> Fin (n + N1) Source #

Weaken the bound of a Fin by 1.

strengthen1Fin :: forall (n :: Nat). SNatI n => Fin ('S n) -> Maybe (Fin n) Source #

With strengthening, we make sure that variable f0 is not used, and we decrement all other indices by 1. This allows us to also decrement the scope by one.

strengthenRecFin :: forall (k :: Nat) (m :: Nat) proxy (n :: Nat). SNat k -> SNat m -> proxy n -> Fin (k + (m + n)) -> Maybe (Fin (k + n)) Source #

We implement strengthening with the following operation that generalizes the induction hypothesis, so that we can strengthen in the middle of the scope. The scope of the Fin should have the form k + (m + n)

Indices in the middle part of the scope m are "strengthened" away.

Orphan instances

ToInt (Fin n) Source #	The `toInteger` instance for Fin has an unnecessary type class constraint (NatI n) for Fin. So we also include this class for simple conversion.
Instance details Methods toInt :: Fin n -> Int Source #