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

LambdaCube.SystemF.Substitution

Documentation

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

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

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

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

substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm Source #

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

substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm Source #