uvmhs-0.0.1.0
Safe HaskellNone
LanguageHaskell2010

UVMHS.Core.Static

Documentation

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

Equations

(a :: k) ≡ (a :: k) = 'True 
(_1 :: k) ≡ (_2 :: k) = '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 :: 𝐍) = Div m n Source #

type (%) (m :: 𝐍) (n :: 𝐍) = Mod m 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 :: forall (m :: 𝐍) (n :: 𝐍). m ≺ n => m < n 

Instances

Instances details
Transitive (<) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

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

withLT :: forall (m :: 𝐍) (n :: 𝐍) a. (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 :: forall (m :: 𝐍) (n :: 𝐍). 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 :: 𝐍). a ≤ a Source #

Transitive (≤) Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

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

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

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

irreflLT :: forall (n :: 𝐍). (n < n) -> Void Source #

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

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

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

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

(♯⊚) :: forall (n₁ :: 𝐍) (n₂ :: 𝐍) (n₃ :: 𝐍). (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 :: Symbol). KnownSymbol s => 𝕊S s Source #

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

AllC (_1 :: a -> Constraint) ('[] :: [a]) = () 
AllC (c :: a -> Constraint) (x ': xs :: [a]) = (c x, AllC c xs) 

data Spine (b :: [a]) where Source #

Constructors

NilSpine :: forall {a}. Spine ('[] :: [a]) 
ConsSpine :: forall {a} (xs :: [a]) (x :: a). Spine xs -> Spine (x ': xs) 

class HasSpine (xs :: [a]) where Source #

Methods

spine :: Spine xs Source #

Instances

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

Defined in UVMHS.Core.Static

Methods

spine :: Spine ('[] :: [a]) 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 :: forall (m :: 𝐍) (n :: 𝐍). 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 (n₂ :: 𝐍). 𝐼S n₁ a -> 𝐼S n₂ a -> 𝐼S (n₁ + n₂) a Source #

NullS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

nullS :: 𝐼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 :: Natural -> k -> Type) where Source #

Methods

nullS :: forall (a :: k). t 0 a Source #

Instances

Instances details
NullS 𝐼S Source # 
Instance details

Defined in UVMHS.Core.Static

Methods

nullS :: 𝐼S 0 a Source #

class SingleS (t :: Natural -> Type -> Type) 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 :: 𝐍 -> k -> Type) where Source #

Methods

(⧺♮) :: forall (n₁ :: 𝐍) (a :: k) (n₂ :: 𝐍). 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 (n₂ :: 𝐍). 𝐼S n₁ a -> 𝐼S n₂ a -> 𝐼S (n₁ + n₂) a Source #