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

Copyright | (c) Galois Inc 2015-2019
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.Ctx.Proofs

Description

This reflects type level proofs involving contexts.

# Documentation

leftId :: forall {k} p (x :: Ctx k). p x -> ((EmptyCtx :: Ctx k) <+> x) :~: x Source #

assoc :: forall {k} p (x :: Ctx k) q (y :: Ctx k) r (z :: Ctx k). p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z) Source #