Noether.Lemmata.TypeFu.DList

Documentation

data The k x

Constructors

The

data Tagged s k x

Constructors

Tagged

Instances

type Cmp * (Tagged s1 _1 _3) (Tagged s2 _ _2)

type Cmp * (Tagged s1 _1 _3) (Tagged s2 _ _2) = Cmp Symbol s1 s2

data DList xs :: Type where

Constructors

Nil :: DList '[]

Tag :: The Symbol s -> The k x -> DList xs -> DList (Tagged s k x ': xs)

nil :: DList '[]

data Foo

Constructors

Bar

Baz

type (**) k x = (The :: The k x)

type (~>) s the = Tag (The :: The Symbol s) the infixr 5

type (|-|) a b = a b infixr 0

type (|<|) a b = a (b Nil) infixr 0

type (|>|) a b = Conv (a b) infixr 0

type family Conv (a :: DList xs) where ...

Equations

Conv (_ :: DList xs) = Sort xs

newtype DList_ xs

Constructors

DList_ (Proxy (Sort xs))

type B = ("index" ~> (Nat ** 1)) |-| (("type" ~> (Type ** Type)) |-| (("afoo" ~> (Nat ** 2)) |-| (("akoe" ~> (Nat ** 2)) |-| (("pqr" ~> (Type ** (Type -> Type))) |<| ("aardvark" ~> ([Type] ** '[Type]))))))

type A = ("index" ~> (Nat ** 1)) |>| (("type" ~> (Type ** Type)) |-| (("afoo" ~> (Nat ** 2)) |-| (("akoe" ~> (Nat ** 2)) |-| (("pqr" ~> (Type ** (Type -> Type))) |<| ("aardvark" ~> ([Type] ** (("b" ~> (Type ** Nat)) |>| (("aa" ~> (Type ** (Type, Type))) |<| ("a" ~> (Nat ** 1))))))))))

class A__ a b | a -> b

Instances

A_ a => A__ a ATag

data ATag

Instances

A_ a => A__ a ATag

data BTag

class A_ a

Instances

(~) [Type] a A => A_ a

f :: A__ A ATag => Proxy Nat

a :: Proxy A