| Portability | GHC |
|---|---|
| Stability | experimental |
| Maintainer | emw4@rice.edu |
| Safe Haskell | Safe-Inferred |
Data.Type.List.Proof.Append
Description
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
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) ctxSource
Appends two Append proofs.