Safe Haskell	Safe-Inferred
Language	Haskell2010

DeBruijn.Lte

Synopsis

data Lte ctx ctx' where
- LZ :: Lte ctx ctx
- LS :: !(Lte ctx ctx') -> Lte ctx (S ctx')

Documentation

data Lte ctx ctx' where Source #

Lte ctx ctx' is evidence that ctx' is smaller than of ctx, less-than-or-equal, and produced by simple skipping only, i.e. nothing is inserted into ctx, only appended to the end.

Constructors

LZ :: Lte ctx ctx
LS :: !(Lte ctx ctx') -> Lte ctx (S ctx')