module LambdaCube.SystemFw_.Lifter ( liftLCValue , liftLCNormal ) where import LambdaCube.SystemFw_.Ast liftLCValue :: LCValue -> LCTerm liftLCValue :: LCValue -> LCTerm liftLCValue (LCValLam LCType t LCTerm b) = LCType -> LCTerm -> LCTerm LCLam LCType t LCTerm b liftLCNormal :: LCNormalTerm -> LCTerm liftLCNormal :: LCNormalTerm -> LCTerm liftLCNormal (LCNormLam LCType t LCNormalTerm b) = LCType -> LCTerm -> LCTerm LCLam LCType t (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ LCNormalTerm -> LCTerm liftLCNormal LCNormalTerm b liftLCNormal (LCNormNeut LCNeutralTerm nt) = LCNeutralTerm -> LCTerm liftLCNeutral LCNeutralTerm nt liftLCNeutral :: LCNeutralTerm -> LCTerm liftLCNeutral :: LCNeutralTerm -> LCTerm liftLCNeutral (LCNeutVar Int x) = Int -> LCTerm LCVar Int x liftLCNeutral (LCNeutApp LCNeutralTerm f LCNormalTerm a) = LCNeutralTerm -> LCTerm liftLCNeutral LCNeutralTerm f LCTerm -> LCTerm -> LCTerm `LCApp` LCNormalTerm -> LCTerm liftLCNormal LCNormalTerm a