Safe Haskell	None
Language	GHC2021

Data.SNat

Contents

Orphan instances

Description

Runtime data that connects to type-level nats.

Synopsis

data Nat
- = Z
- | S Nat
toNatural :: Nat -> Natural
fromNatural :: Natural -> 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
snatToNat :: forall (n :: Nat). SNat n -> Nat
class SNatI (n :: Nat) where
- induction :: f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
snat :: forall (n :: Nat). SNatI n => SNat n
withSNat :: forall (n :: Nat) r. SNat n -> (SNatI n => r) -> r
reify :: Nat -> (forall (n :: Nat). SNatI n => Proxy n -> r) -> r
reflect :: forall (n :: Nat) proxy. SNatI n => proxy n -> Nat
type family (n :: Nat) + (m :: Nat) :: Nat where ...
type N0 = 'Z
type N1 = 'S N0
type N2 = 'S N1
type N3 = 'S N2
s0 :: SNat N0
s1 :: SNat N1
s2 :: SNat N2
s3 :: SNat N3
sPlus :: forall (n1 :: Nat) (n2 :: Nat). SNat n1 -> SNat n2 -> SNat (n1 + n2)
axiomPlusZ :: forall (m :: Nat). (m + 'Z) :~: m
axiomAssoc :: forall (p :: Nat) (m :: Nat) (n :: Nat). (p + (m + n)) :~: ((p + m) + n)
data SNat_ (n :: Nat) where
- SZ_ :: SNat_ 'Z
- SS_ :: forall (n1 :: Nat). SNat n1 -> SNat_ ('S n1)
snat_ :: forall (n :: Nat). SNat n -> SNat_ n
prev :: forall (n :: Nat). SNat ('S n) -> SNat n
next :: forall (n :: Nat). SNat n -> SNat ('S n)
class ToInt a where
- toInt :: a -> Int

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

toNatural :: Nat -> Natural #

Convert Nat to Natural

>>> toNatural 0
0

>>> toNatural 2
2

>>> toNatural $ S $ S $ Z
2

fromNatural :: Natural -> Nat #

Convert Natural to Nat

>>> fromNatural 4
4

>>> explicitShow (fromNatural 4)
"S (S (S (S Z)))"

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

snatToNat :: forall (n :: Nat). SNat n -> Nat #

Convert SNat to Nat.

>>> snatToNat (snat :: SNat Nat1)
1

class SNatI (n :: Nat) where #

Implicit SNat.

In an unorthodox singleton way, it actually provides an induction function.

The induction should often be fully inlined. See test/Inspection.hs.

>>> :set -XPolyKinds
>>> newtype Const a b = Const a deriving (Show)
>>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3
Const 6

Methods

induction #

Arguments

:: f 'Z	zero case
-> (forall (m :: Nat). SNatI m => f m -> f ('S m))	induction step
-> f n

Instances

Instances details

SNatI 'Z
Instance details Defined in Data.Type.Nat Methods induction :: f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f 'Z #
SNatI n => SNatI ('S n)
Instance details Defined in Data.Type.Nat Methods induction :: f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f ('S n) #

snat :: forall (n :: Nat). SNatI n => SNat n #

Construct explicit SNat value.

withSNat :: forall (n :: Nat) r. SNat n -> (SNatI n => r) -> r #

Constructor SNatI dictionary from SNat.

Since: fin-0.0.3

reify :: Nat -> (forall (n :: Nat). SNatI n => Proxy n -> r) -> r #

Reify Nat.

>>> reify nat3 reflect
3

reflect :: forall (n :: Nat) proxy. SNatI n => proxy n -> Nat #

Reflect type-level Nat to the term level.

type family (n :: Nat) + (m :: Nat) :: Nat where ... Source #

Notation for the addition of naturals.

Equations

m + n = Plus m n

type N0 = 'Z Source #

type N1 = 'S N0 Source #

type N2 = 'S N1 Source #

type N3 = 'S N2 Source #

s0 :: SNat N0 Source #

s1 :: SNat N1 Source #

s2 :: SNat N2 Source #

s3 :: SNat N3 Source #

sPlus :: forall (n1 :: Nat) (n2 :: Nat). SNat n1 -> SNat n2 -> SNat (n1 + n2) Source #

Addition of singleton naturals.

axiomPlusZ :: forall (m :: Nat). (m + 'Z) :~: m Source #

'0' is identity element for +

axiomAssoc :: forall (p :: Nat) (m :: Nat) (n :: Nat). (p + (m + n)) :~: ((p + m) + n) Source #

+ is associative.

data SNat_ (n :: Nat) where Source #

View pattern allowing pattern matching on naturals. See snat_.

Constructors

SZ_ :: SNat_ 'Z
SS_ :: forall (n1 :: Nat). SNat n1 -> SNat_ ('S n1)

snat_ :: forall (n :: Nat). SNat n -> SNat_ n Source #

View pattern allowing pattern matching on naturals.

f :: forall p. SNat p -> ...
f SZ = ...
f (snat_ -> SS_ m) = ...

prev :: forall (n :: Nat). SNat ('S n) -> SNat n Source #

Predecessor of a natural.

next :: forall (n :: Nat). SNat n -> SNat ('S n) Source #

Successor of a natural.

class ToInt a where Source #

Conversion to Int.

Methods

toInt :: a -> Int Source #

Instances

Instances details

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 #
ToInt (SNat n) Source #
Instance details Defined in Data.SNat Methods toInt :: SNat n -> Int Source #

Orphan instances

SNatI n => Arbitrary (SNat n) Source #
Instance details Methods arbitrary :: Gen (SNat n) # shrink :: SNat n -> [SNat n] #