Portability | GHC |
---|---|
Stability | experimental |
Maintainer | emw4@rice.edu |
Safe Haskell | Safe-Infered |
Proofs regarding a type list as an append of two others.
- data Append ctx1 ctx2 ctx where
- 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
- appendPf :: Append ctx1 ctx2 ctx -> ctx :=: (ctx1 :++: ctx2)
- length :: Append ctx1 ctx2 ctx3 -> Int
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) |
trans :: Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctxSource
Appends two Append
proofs.