{-|
Description : type-level proofs involving contexts
Copyright   : (c) Galois, Inc 2015-2019
Maintainer  : Joe Hendrix <jhendrix@galois.com>

This reflects type level proofs involving contexts.
-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
module Data.Parameterized.Ctx.Proofs
  ( leftId
  , assoc
  ) where

import Data.Type.Equality

import Data.Parameterized.Axiom
import Data.Parameterized.Ctx

leftId :: p x -> (EmptyCtx <+> x) :~: x
leftId :: p x -> (EmptyCtx <+> x) :~: x
leftId p x
_ = (EmptyCtx <+> x) :~: x
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom

assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z
assoc :: p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
assoc p x
_ q y
_ r z
_ = (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom