DeBruijn.Lte

Documentation

data Lte ctx ctx' where

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')