Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Length

Description

A singleton-esque type for representing lengths of type-level lists, irrespective of the actual types in that list.

Documentation

data Length :: [k] -> * where Source

Constructors

LZ :: Length Ø
LS :: !(Length as) -> Length (a :< as)

Instances

Read1 [k] (Length k) Source
Show1 [k] (Length k) Source
Ord1 [k] (Length k) Source
Eq1 [k] (Length k) Source
Known [k] (Length k) (Ø k) Source
Known [k] (Length k) as => Known [k] (Length k) ((:<) k a as) Source
Eq (Length k as) Source
Ord (Length k as) Source
Show (Length k as) Source
type KnownC [k] (Length k) (Ø k) = ØC
type KnownC [k] (Length k) ((:<) k a as) = Known [k] (Length k) as Source

elimLength :: p Ø -> (forall x xs. Length xs -> p xs -> p (x :< xs)) -> Length as -> p as Source