Portability | GHC |
---|---|
Stability | experimental |
Maintainer | emw4@rice.edu |
Proofs regarding a type list as an append of two others.
Documentation
data Append ctx1 ctx2 ctx whereSource
An Append ctx1 ctx2 ctx
is a "proof" that ctx = ctx1
.
:++:
ctx2
Append_Base :: Append ctx Nil ctx | |
Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a) |