uvmhs-0.0.0.0
Safe HaskellSafe-Inferred
LanguageHaskell2010

UVMHS.Core.Static

Documentation

type family (a :: k) ≡ (b :: k) where ... Source #

Equations

a ≡ a = 'True 
_ ≡ _ = 'False 

type family (x :: 𝔹) ⩔ (y :: 𝔹) where ... Source #

Equations

'False ⩔ x = x 
x ⩔ 'False = x 
'True ⩔ 'True = 'True 

type family (x :: 𝔹) ⩓ (y :: 𝔹) where ... Source #

Equations

'True ⩓ x = x 
x ⩓ 'True = x 
'False ⩓ 'False = 'False 

type 𝐍 = Nat Source #

type 𝐒 = Symbol Source #

type (+) (m :: 𝐍) (n :: 𝐍) = m + n Source #

type (×) (m :: 𝐍) (n :: 𝐍) = m * n Source #

type (^) (m :: 𝐍) (n :: 𝐍) = m ^ n Source #

type (-) (m :: 𝐍) (n :: 𝐍) = m - n Source #

type (/) (m :: 𝐍) (n :: 𝐍) = m `Div` n Source #

type (%) (m :: 𝐍) (n :: 𝐍) = m `Mod` n Source #

type Log2 (n :: 𝐍) = Log2 n Source #

type (⋚) (m :: 𝐍) (n :: 𝐍) = CmpNat m n Source #

type (≺) (m :: 𝐍) (n :: 𝐍) = ((m ⋚ n) ≡ 'LT) ~ 'True infix 4 Source #

type (≍) (m :: 𝐍) (n :: 𝐍) = ((m ⋚ n) ≡ 'EQ) ~ 'True infix 4 Source #

type (≻) (m :: 𝐍) (n :: 𝐍) = ((m ⋚ n) ≡ 'GT) ~ 'True infix 4 Source #

type (≼) (m :: 𝐍) (n :: 𝐍) = (((m ⋚ n) ≡ 'LT) ⩔ ((m ⋚ n) ≡ 'EQ)) ~ 'True infix 4 Source #

wnlt_UNSAFE :: forall m n. P m -> P n -> W (m ≺ n) Source #

wneq_UNSAFE :: forall m n. P m -> P n -> W (m ≍ n) Source #

wngt_UNSAFE :: forall m n. P m -> P n -> W (m ≻ n) Source #

wnlte_UNSAFE :: forall m n. P m -> P n -> W (m ≼ n) Source #

data (m :: 𝐍) < (n :: 𝐍) where infix 4 Source #

Constructors

W_LT :: m ≺ n => m < n 

Instances

Instances details
Transitive (<) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

(⊚) :: forall (b :: k) (c :: k) (a :: k). (b < c) -> (a < b) -> a < c Source #

withLT :: (m < n) -> (m ≺ n => a) -> a Source #

nlt_UNSAFE :: forall m n. P m -> P n -> m < n Source #

data (m :: 𝐍) ≤ (n :: 𝐍) where infix 4 Source #

Constructors

W_LTE :: m ≼ n => m ≤ n 

Instances

Instances details
Category (≤) Source # 
Instance details

Defined in UVMHS.Core.Static

Reflexive (≤) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

refl :: forall (a :: k). a ≤ a Source #

Transitive (≤) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

(⊚) :: forall (b :: k) (c :: k) (a :: k). (b ≤ c) -> (a ≤ b) -> a ≤ c Source #

withLTE :: (m ≤ n) -> (m ≼ n => a) -> a Source #

nlte_UNSAFE :: forall m n. P m -> P n -> m ≤ n Source #

irreflLT :: (n < n) -> Void Source #

weakenLT :: (n₁ < n₂) -> n₁ ≤ n₂ Source #

succLT :: (n₁ < n₂) -> (n₁ + 1) ≤ n₂ Source #

succLTE :: (n₁ ≤ n₂) -> n₁ < (n₂ + 1) Source #

(⊚♯) :: (n₁ ≤ n₂) -> (n₂ < n₃) -> n₁ < n₃ Source #

(♯⊚) :: (n₁ < n₂) -> (n₂ ≤ n₃) -> n₁ < n₃ Source #

newtype ℕS (n :: 𝐍) Source #

Constructors

ℕS_UNSAFE 

Fields

newtype ℕ64S (n :: 𝐍) Source #

Constructors

ℕ64S_UNSAFE 

Fields

newtype 𝕊S (s :: 𝐒) Source #

Constructors

𝕊S_UNSAFE 

Fields

class KnownNat n => 𝒩 (n :: 𝐍) where Source #

Methods

reifyℕ :: P n -> ℕ Source #

Instances

Instances details
KnownNat n => 𝒩 n Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

reifyℕ :: P n -> ℕ Source #

class KnownNat n => 𝒩64 (n :: 𝐍) where Source #

Methods

reifyℕ64 :: P n -> ℕ64 Source #

Instances

Instances details
KnownNat n => 𝒩64 n Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

reifyℕ64 :: P n -> ℕ64 Source #

class KnownSymbol s => 𝒮 (s :: 𝐒) where Source #

Methods

reify𝕊 :: P s -> 𝕊 Source #

Instances

Instances details
KnownSymbol s => 𝒮 s Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

reify𝕊 :: P s -> 𝕊 Source #

compare𝐍 :: forall (a :: 𝐍) (b :: 𝐍). (𝒩 a, 𝒩 b) => 𝑂 (a ≟ b) Source #

𝕟s :: forall n. 𝒩 n => ℕS n Source #

𝕟d :: ℕ -> (forall n. 𝒩 n => ℕS n -> a) -> a Source #

𝕟64s :: forall n. 𝒩64 n => ℕ64S n Source #

𝕟64d :: ℕ64 -> (forall n. 𝒩64 n => ℕ64S n -> a) -> a Source #

𝕤s :: forall s. KnownSymbol s => 𝕊S s Source #

𝕤sd :: 𝕊 -> (forall s. 𝒮 s => 𝕊S s -> a) -> a Source #

type family (xs :: [a]) ⧺ (ys :: [a]) :: [a] where ... Source #

Equations

'[] ⧺ ys = ys 
(x ': xs) ⧺ ys = x ': (xs ⧺ ys) 

type family Sum (ns :: [𝐍]) where ... Source #

Equations

Sum '[] = 0 
Sum (n ': ns) = n + Sum ns 

type family Prod (ns :: [𝐍]) where ... Source #

Equations

Prod '[] = 1 
Prod (n ': ns) = n × Prod ns 

type family AllC (c :: a -> Constraint) (xs :: [a]) :: Constraint where ... Source #

Equations

AllC _ '[] = () 
AllC c (x ': xs) = (c x, AllC c xs) 

data Spine :: [a] -> ★ where Source #

Constructors

NilSpine :: Spine '[] 
ConsSpine :: Spine xs -> Spine (x ': xs) 

class HasSpine xs where Source #

Methods

spine :: Spine xs Source #

Instances

Instances details
HasSpine ('[] :: [a]) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

spine :: Spine '[] Source #

HasSpine xs => HasSpine (x ': xs :: [a]) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

spine :: Spine (x ': xs) Source #

newtype 𝕀64 (n :: 𝐍) Source #

Constructors

𝕀64_UNSAFE 

Fields

Instances

Instances details
Access (𝕀64 n) a (𝕍SV n a) Source # 
Instance details

Defined in UVMHS.Core.VectorStatic

Methods

(⋕) :: 𝕍SV n a -> 𝕀64 n -> a Source #

Storable a => Access (𝕀64 n) a (𝕌S n a) Source # 
Instance details

Defined in UVMHS.Core.VectorStatic

Methods

(⋕) :: 𝕌S n a -> 𝕀64 n -> a Source #

Access (𝕀64 n) a (𝕍S n a) Source # 
Instance details

Defined in UVMHS.Core.VectorStatic

Methods

(⋕) :: 𝕍S n a -> 𝕀64 n -> a Source #

𝕚64 :: forall m n. m ≺ n => ℕ64S m -> 𝕀64 n Source #

𝕚64d :: forall n. 𝒩64 n => ℕ64 -> 𝑂 (𝕀64 n) Source #

𝕟64di :: forall n a. 𝕀64 n -> (forall m. m ≺ n => ℕ64S m -> a) -> a Source #

upto𝕀64 :: forall n. 𝒩64 n => ℕ64S n -> 𝐼S n (𝕀64 n) Source #

wk𝕀64 :: m ≼ n => 𝕀64 m -> 𝕀64 n Source #

newtype 𝐼S (n :: 𝐍) a Source #

Constructors

𝐼S_UNSAFE 

Fields

Instances

Instances details
SingleS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

𝔢 :: a -> 𝐼S 1 a Source #

AppendS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

(⧺♮) :: forall (n₁ :: 𝐍) (a :: k) (n₂ :: 𝐍). 𝐼S n₁ a -> 𝐼S n₂ a -> 𝐼S (n₁ + n₂) a Source #

NullS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

nullS :: forall (a :: k). 𝐼S 0 a Source #

ToIter a (𝐼S n a) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

iter :: 𝐼S n a -> 𝐼 a Source #

Functor (𝐼S n) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

map :: (a -> b) -> 𝐼S n a -> 𝐼S n b Source #

Show a => Show (𝐼S n a) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

showsPrec :: Int -> 𝐼S n a -> ShowS #

show :: 𝐼S n a -> String #

showList :: [𝐼S n a] -> ShowS #

class NullS t where Source #

Methods

nullS :: t 0 a Source #

Instances

Instances details
NullS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

nullS :: forall (a :: k). 𝐼S 0 a Source #

class SingleS t where Source #

Methods

𝔢 :: a -> t 1 a Source #

Instances

Instances details
SingleS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

𝔢 :: a -> 𝐼S 1 a Source #

class AppendS t where Source #

Methods

(⧺♮) :: t n₁ a -> t n₂ a -> t (n₁ + n₂) a Source #

Instances

Instances details
AppendS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

(⧺♮) :: forall (n₁ :: 𝐍) (a :: k) (n₂ :: 𝐍). 𝐼S n₁ a -> 𝐼S n₂ a -> 𝐼S (n₁ + n₂) a Source #