Zabt.Arity

Arities are type-level naturals used to describe the number of variables that must be immediately bound at a Term.

Documentation

data Arity

Constructors

G

B Arity

type G = G

type B a = B a

type A0 = G

type A1 = B G

type A2 = B A1

type A3 = B A2

type family DownTo (c :: * -> Constraint) (x :: Arity -> *) (a :: Arity) :: Constraint where ...

The DownTo type family makes it easier to declare type constraints over families of arities.

Equations

DownTo c x G = c (x G)

DownTo c x (B a) = (c (x (B a)), DownTo c x a)