{-# LANGUAGE Trustworthy #-} module DeBruijn.RenExtras ( weakenUsingSize, ) where import DeBruijn.Ctx import DeBruijn.Ren import DeBruijn.Size import Unsafe.Coerce (unsafeCoerce) -- | Weaken closed term to arbitrary context. -- -- Note: this has different requirements than 'sinkSize'. weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx weakenUsingSize :: forall (t :: Ctx -> *) (ctx :: Ctx). Renamable t => Size ctx -> t EmptyCtx -> t ctx weakenUsingSize Size ctx _ = t EmptyCtx -> t ctx forall a b. a -> b unsafeCoerce