Copyright | Copyright (C) 2015 Kyle Carter |
---|---|

License | BSD3 |

Maintainer | Kyle Carter <kylcarte@indiana.edu> |

Stability | experimental |

Portability | RankNTypes |

Safe Haskell | None |

Language | Haskell2010 |

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 #

(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |

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 WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |

type KnownC [k] (Length k) (Ø k) Source # | |

type KnownC [k] (Length k) ((:<) k a as) Source # | |