parameterized-utils-1.0.0: Classes and data structures for working with data-kind indexed types

Copyright	(c) Galois Inc 2015
Maintainer	Joe Hendrix <[email protected]>
Safe Haskell	None
Language	Haskell98

Data.Parameterized.Ctx.Proofs

Description

This reflects type level proofs involving contexts.

Documentation

leftId :: p x -> (EmptyCtx <+> x) :~: x Source #

assoc :: p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z) Source #