debruijn-safe-0.1: de Bruijn indices and levels
Safe HaskellSafe-Inferred
LanguageHaskell2010

DeBruijn.Lte

Synopsis

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