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

Copyright(c) Galois Inc 2015-2019
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell98

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 #