lambda-cube-0.3.0.0: Haskell implementation of (some of) lambda cube calculi
Safe HaskellNone
LanguageHaskell2010

LambdaCube.SystemF.Substitution

Documentation

substituteType :: LCType -> Int -> LCTerm -> LCTerm Source #

substituteTypeInType :: LCType -> Int -> LCType -> LCType Source #

substituteValue :: LCValue -> Int -> LCTerm -> LCTerm Source #

substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm Source #

substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm Source #

shiftType :: (LCType, Int) -> LCType Source #