{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module QLinear.Index where
import Data.Proxy
import qualified GHC.Natural as Natural
import GHC.TypeNats
data Index (i :: Nat) (j :: Nat) = Index
instance forall i j. (KnownNat i, KnownNat j) => Show (Index i j) where
show :: Index i j -> String
show _ = "Index " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> " " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
j
where
i :: Natural
i = Proxy i -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy i
forall k (t :: k). Proxy t
Proxy @i)
j :: Natural
j = Proxy j -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy j
forall k (t :: k). Proxy t
Proxy @j)