Data.Type.List.Proof.Append

Proofs regarding a type list as an append of two others.

Documentation

data Append ctx1 ctx2 ctx where

An Append ctx1 ctx2 ctx is a "proof" that ctx = ctx1 :++: ctx2.

Constructors

Append_Base :: Append ctx Nil ctx

Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)

trans :: Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx

Appends two Append proofs.

length :: Append ctx1 ctx2 ctx3 -> Int

Returns the length of an Append proof.