parameterized-utils-2.1.3.0: Classes and data structures for working with data-kind indexed types
Copyright(c) Galois Inc 2015-2019
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell2010

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 #