-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Haskell implementation of (some of) lambda cube calculi -- -- Haskell implementation of the following 4 lambda calculi: -- --
    --
  1. Simply typed lambda calculus
    2. --
  2. System F
    3. --
  3. System F omega underbar
    4. --
  4. System F omega
    5. --
@package lambda-cube @version 0.3.0.0 module LambdaCube.Common.Parser type Parser = Parsec Void Text topParser :: Parser a -> Parser a parenthesized :: Parser a -> Parser a identifier :: Parser Text rightArrow :: Parser Text atsignBackslash :: Parser Text backslash :: Parser Char atsign :: Parser Char sharp :: Parser Char colon :: Parser Char dot :: Parser Char openParenthesis :: Parser Char closeParenthesis :: Parser Char exclamationMark :: Parser Char comma :: Parser Char asterisk :: Parser Char dollarsign :: Parser Char module LambdaCube.Common.PrettyPrinter wrapIfSpaced :: Bool -> [Text] -> Text wrapIf :: Bool -> Text -> Text wrap :: Text -> Text spaced :: [Text] -> Text module LambdaCube.Common.TH qExpBase :: Data a => Parser a -> (forall b. Data b => b -> Maybe ExpQ) -> String -> ExpQ converterBase :: Data b => b -> Maybe ExpQ module LambdaCube.STLC.Ast data ExtLCTerm ExtLCVar :: Text -> ExtLCTerm ExtLCLam :: Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm ExtLCApp :: ExtLCTerm -> ExtLCTerm -> ExtLCTerm ExtLCMVar :: String -> ExtLCTerm infixl 6 `ExtLCApp` data ExtLCType ExtLCBase :: ExtLCType ExtLCArr :: ExtLCType -> ExtLCType -> ExtLCType ExtLCMTVar :: String -> ExtLCType infixr 5 `ExtLCArr` data LCTerm LCVar :: Int -> LCTerm LCLam :: LCType -> LCTerm -> LCTerm LCApp :: LCTerm -> LCTerm -> LCTerm infixl 6 `LCApp` data LCType LCBase :: LCType LCArr :: LCType -> LCType -> LCType infixr 5 `LCArr` data LCValue LCValLam :: LCType -> LCTerm -> LCValue data LCNormalTerm LCNormLam :: LCType -> LCNormalTerm -> LCNormalTerm LCNormNeut :: LCNeutralTerm -> LCNormalTerm data LCNeutralTerm LCNeutVar :: Int -> LCNeutralTerm LCNeutApp :: LCNeutralTerm -> LCNormalTerm -> LCNeutralTerm infixl 6 `LCNeutApp` instance Language.Haskell.TH.Syntax.Lift LambdaCube.STLC.Ast.ExtLCType instance Data.Data.Data LambdaCube.STLC.Ast.ExtLCType instance GHC.Show.Show LambdaCube.STLC.Ast.ExtLCType instance GHC.Classes.Eq LambdaCube.STLC.Ast.ExtLCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.STLC.Ast.ExtLCTerm instance Data.Data.Data LambdaCube.STLC.Ast.ExtLCTerm instance GHC.Show.Show LambdaCube.STLC.Ast.ExtLCTerm instance GHC.Classes.Eq LambdaCube.STLC.Ast.ExtLCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.STLC.Ast.LCType instance Data.Data.Data LambdaCube.STLC.Ast.LCType instance GHC.Show.Show LambdaCube.STLC.Ast.LCType instance GHC.Classes.Eq LambdaCube.STLC.Ast.LCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.STLC.Ast.LCTerm instance Data.Data.Data LambdaCube.STLC.Ast.LCTerm instance GHC.Show.Show LambdaCube.STLC.Ast.LCTerm instance GHC.Classes.Eq LambdaCube.STLC.Ast.LCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.STLC.Ast.LCValue instance Data.Data.Data LambdaCube.STLC.Ast.LCValue instance GHC.Show.Show LambdaCube.STLC.Ast.LCValue instance GHC.Classes.Eq LambdaCube.STLC.Ast.LCValue instance Language.Haskell.TH.Syntax.Lift LambdaCube.STLC.Ast.LCNormalTerm instance Data.Data.Data LambdaCube.STLC.Ast.LCNormalTerm instance GHC.Show.Show LambdaCube.STLC.Ast.LCNormalTerm instance GHC.Classes.Eq LambdaCube.STLC.Ast.LCNormalTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.STLC.Ast.LCNeutralTerm instance Data.Data.Data LambdaCube.STLC.Ast.LCNeutralTerm instance GHC.Show.Show LambdaCube.STLC.Ast.LCNeutralTerm instance GHC.Classes.Eq LambdaCube.STLC.Ast.LCNeutralTerm module LambdaCube.STLC.Elaborator elaborate :: ExtLCTerm -> LCTerm elaborateType :: ExtLCType -> LCType module LambdaCube.STLC.Lifter liftLCValue :: LCValue -> LCTerm liftLCNormal :: LCNormalTerm -> LCTerm module LambdaCube.STLC.Parser pTopTerm :: Parser ExtLCTerm pTopType :: Parser ExtLCType module LambdaCube.STLC.PrettyPrinter prettyUnnamedTerm :: LCTerm -> Text prettyShowUnnamedTerm :: LCTerm -> String prettyUnnamedType :: LCType -> Text prettyShowUnnamedType :: LCType -> String module LambdaCube.STLC.Substitution substituteValue :: LCValue -> Int -> LCTerm -> LCTerm substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm module LambdaCube.STLC.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.STLC.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.STLC.TH qTerm :: QuasiQuoter qType :: QuasiQuoter module LambdaCube.STLC.TypeChecker infer :: LCTerm -> LCType module LambdaCube.STLC module LambdaCube.SystemF.Ast data ExtLCTerm ExtLCVar :: Text -> ExtLCTerm ExtLCLam :: Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm ExtLCApp :: ExtLCTerm -> ExtLCTerm -> ExtLCTerm ExtLCTLam :: Text -> ExtLCTerm -> ExtLCTerm ExtLCTApp :: ExtLCTerm -> ExtLCType -> ExtLCTerm ExtLCMVar :: String -> ExtLCTerm infixl 6 `ExtLCTApp` infixl 6 `ExtLCApp` data ExtLCType ExtLCBase :: ExtLCType ExtLCTVar :: Text -> ExtLCType ExtLCArr :: ExtLCType -> ExtLCType -> ExtLCType ExtLCUniv :: Text -> ExtLCType -> ExtLCType ExtLCMTVar :: String -> ExtLCType infixr 5 `ExtLCArr` data LCTerm LCVar :: Int -> LCTerm LCLam :: LCType -> LCTerm -> LCTerm LCApp :: LCTerm -> LCTerm -> LCTerm LCTLam :: LCTerm -> LCTerm LCTApp :: LCTerm -> LCType -> LCTerm infixl 6 `LCTApp` infixl 6 `LCApp` data LCType LCBase :: LCType LCTVar :: Int -> LCType LCArr :: LCType -> LCType -> LCType LCUniv :: LCType -> LCType infixr 5 `LCArr` data LCValue LCValLam :: LCType -> LCTerm -> LCValue LCValTLam :: LCTerm -> LCValue data LCNormalTerm LCNormLam :: LCType -> LCNormalTerm -> LCNormalTerm LCNormTLam :: LCNormalTerm -> LCNormalTerm LCNormNeut :: LCNeutralTerm -> LCNormalTerm data LCNeutralTerm LCNeutVar :: Int -> LCNeutralTerm LCNeutApp :: LCNeutralTerm -> LCNormalTerm -> LCNeutralTerm LCNeutTApp :: LCNeutralTerm -> LCType -> LCNeutralTerm infixl 6 `LCNeutTApp` infixl 6 `LCNeutApp` instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemF.Ast.ExtLCType instance Data.Data.Data LambdaCube.SystemF.Ast.ExtLCType instance GHC.Show.Show LambdaCube.SystemF.Ast.ExtLCType instance GHC.Classes.Eq LambdaCube.SystemF.Ast.ExtLCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemF.Ast.ExtLCTerm instance Data.Data.Data LambdaCube.SystemF.Ast.ExtLCTerm instance GHC.Show.Show LambdaCube.SystemF.Ast.ExtLCTerm instance GHC.Classes.Eq LambdaCube.SystemF.Ast.ExtLCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemF.Ast.LCType instance Data.Data.Data LambdaCube.SystemF.Ast.LCType instance GHC.Show.Show LambdaCube.SystemF.Ast.LCType instance GHC.Classes.Eq LambdaCube.SystemF.Ast.LCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemF.Ast.LCTerm instance Data.Data.Data LambdaCube.SystemF.Ast.LCTerm instance GHC.Show.Show LambdaCube.SystemF.Ast.LCTerm instance GHC.Classes.Eq LambdaCube.SystemF.Ast.LCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemF.Ast.LCValue instance Data.Data.Data LambdaCube.SystemF.Ast.LCValue instance GHC.Show.Show LambdaCube.SystemF.Ast.LCValue instance GHC.Classes.Eq LambdaCube.SystemF.Ast.LCValue instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemF.Ast.LCNormalTerm instance Data.Data.Data LambdaCube.SystemF.Ast.LCNormalTerm instance GHC.Show.Show LambdaCube.SystemF.Ast.LCNormalTerm instance GHC.Classes.Eq LambdaCube.SystemF.Ast.LCNormalTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemF.Ast.LCNeutralTerm instance Data.Data.Data LambdaCube.SystemF.Ast.LCNeutralTerm instance GHC.Show.Show LambdaCube.SystemF.Ast.LCNeutralTerm instance GHC.Classes.Eq LambdaCube.SystemF.Ast.LCNeutralTerm module LambdaCube.SystemF.Elaborator elaborate :: ExtLCTerm -> LCTerm elaborateType :: [Text] -> ExtLCType -> LCType module LambdaCube.SystemF.Lifter liftLCValue :: LCValue -> LCTerm liftLCNormal :: LCNormalTerm -> LCTerm module LambdaCube.SystemF.Parser pTopTerm :: Parser ExtLCTerm pTopType :: Parser ExtLCType module LambdaCube.SystemF.PrettyPrinter prettyUnnamedTerm :: LCTerm -> Text prettyShowUnnamedTerm :: LCTerm -> String prettyUnnamedType :: LCType -> Text prettyShowUnnamedType :: LCType -> String module LambdaCube.SystemF.Substitution substituteType :: LCType -> Int -> LCTerm -> LCTerm substituteTypeInType :: LCType -> Int -> LCType -> LCType substituteValue :: LCValue -> Int -> LCTerm -> LCTerm substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm shiftType :: (LCType, Int) -> LCType module LambdaCube.SystemF.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.SystemF.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.SystemF.TH qTerm :: QuasiQuoter qType :: QuasiQuoter module LambdaCube.SystemF.TypeChecker infer :: LCTerm -> LCType module LambdaCube.SystemF module LambdaCube.SystemFw.Ast data ExtLCTerm ExtLCVar :: Text -> ExtLCTerm ExtLCLam :: Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm ExtLCApp :: ExtLCTerm -> ExtLCTerm -> ExtLCTerm ExtLCTLam :: Text -> ExtLCKind -> ExtLCTerm -> ExtLCTerm ExtLCTApp :: ExtLCTerm -> ExtLCType -> ExtLCTerm ExtLCMVar :: String -> ExtLCTerm infixl 6 `ExtLCTApp` infixl 6 `ExtLCApp` data ExtLCType ExtLCBase :: ExtLCType ExtLCTVar :: Text -> ExtLCType ExtLCArr :: ExtLCType -> ExtLCType -> ExtLCType ExtLCUniv :: Text -> ExtLCKind -> ExtLCType -> ExtLCType ExtLCTTLam :: Text -> ExtLCKind -> ExtLCType -> ExtLCType ExtLCTTApp :: ExtLCType -> ExtLCType -> ExtLCType ExtLCMTVar :: String -> ExtLCType infixl 6 `ExtLCTTApp` infixr 5 `ExtLCArr` data ExtLCKind ExtLCStar :: ExtLCKind ExtLCKArr :: ExtLCKind -> ExtLCKind -> ExtLCKind ExtLCMKVar :: String -> ExtLCKind infixr 5 `ExtLCKArr` data LCTerm LCVar :: Int -> LCTerm LCLam :: LCType -> LCTerm -> LCTerm LCApp :: LCTerm -> LCTerm -> LCTerm LCTLam :: LCKind -> LCTerm -> LCTerm LCTApp :: LCTerm -> LCType -> LCTerm infixl 6 `LCTApp` infixl 6 `LCApp` data LCType LCBase :: LCType LCTVar :: Int -> LCType LCArr :: LCType -> LCType -> LCType LCUniv :: LCKind -> LCType -> LCType LCTTLam :: LCKind -> LCType -> LCType LCTTApp :: LCType -> LCType -> LCType infixl 6 `LCTTApp` infixr 5 `LCArr` data LCKind LCStar :: LCKind LCKArr :: LCKind -> LCKind -> LCKind infixr 5 `LCKArr` data LCValue LCValLam :: LCType -> LCTerm -> LCValue LCValTLam :: LCKind -> LCTerm -> LCValue data LCNormalTerm LCNormLam :: LCType -> LCNormalTerm -> LCNormalTerm LCNormTLam :: LCKind -> LCNormalTerm -> LCNormalTerm LCNormNeut :: LCNeutralTerm -> LCNormalTerm data LCNeutralTerm LCNeutVar :: Int -> LCNeutralTerm LCNeutApp :: LCNeutralTerm -> LCNormalTerm -> LCNeutralTerm LCNeutTApp :: LCNeutralTerm -> LCType -> LCNeutralTerm infixl 6 `LCNeutTApp` infixl 6 `LCNeutApp` instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.ExtLCKind instance Data.Data.Data LambdaCube.SystemFw.Ast.ExtLCKind instance GHC.Show.Show LambdaCube.SystemFw.Ast.ExtLCKind instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.ExtLCKind instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.ExtLCType instance Data.Data.Data LambdaCube.SystemFw.Ast.ExtLCType instance GHC.Show.Show LambdaCube.SystemFw.Ast.ExtLCType instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.ExtLCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.ExtLCTerm instance Data.Data.Data LambdaCube.SystemFw.Ast.ExtLCTerm instance GHC.Show.Show LambdaCube.SystemFw.Ast.ExtLCTerm instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.ExtLCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.LCKind instance Data.Data.Data LambdaCube.SystemFw.Ast.LCKind instance GHC.Show.Show LambdaCube.SystemFw.Ast.LCKind instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.LCKind instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.LCType instance Data.Data.Data LambdaCube.SystemFw.Ast.LCType instance GHC.Show.Show LambdaCube.SystemFw.Ast.LCType instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.LCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.LCTerm instance Data.Data.Data LambdaCube.SystemFw.Ast.LCTerm instance GHC.Show.Show LambdaCube.SystemFw.Ast.LCTerm instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.LCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.LCValue instance Data.Data.Data LambdaCube.SystemFw.Ast.LCValue instance GHC.Show.Show LambdaCube.SystemFw.Ast.LCValue instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.LCValue instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.LCNormalTerm instance Data.Data.Data LambdaCube.SystemFw.Ast.LCNormalTerm instance GHC.Show.Show LambdaCube.SystemFw.Ast.LCNormalTerm instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.LCNormalTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw.Ast.LCNeutralTerm instance Data.Data.Data LambdaCube.SystemFw.Ast.LCNeutralTerm instance GHC.Show.Show LambdaCube.SystemFw.Ast.LCNeutralTerm instance GHC.Classes.Eq LambdaCube.SystemFw.Ast.LCNeutralTerm module LambdaCube.SystemFw.Elaborator elaborate :: ExtLCTerm -> LCTerm elaborateType :: [Text] -> ExtLCType -> LCType elaborateKind :: ExtLCKind -> LCKind module LambdaCube.SystemFw.Lifter liftLCValue :: LCValue -> LCTerm liftLCNormal :: LCNormalTerm -> LCTerm module LambdaCube.SystemFw.Parser pTopTerm :: Parser ExtLCTerm pTopType :: Parser ExtLCType pTopKind :: Parser ExtLCKind module LambdaCube.SystemFw.PrettyPrinter prettyUnnamedTerm :: LCTerm -> Text prettyShowUnnamedTerm :: LCTerm -> String prettyUnnamedType :: LCType -> Text prettyShowUnnamedType :: LCType -> String prettyUnnamedKind :: LCKind -> Text prettyShowUnnamedKind :: LCKind -> String module LambdaCube.SystemFw.Substitution substituteType :: LCType -> Int -> LCTerm -> LCTerm substituteTypeInType :: LCType -> Int -> LCType -> LCType substituteValue :: LCValue -> Int -> LCTerm -> LCTerm substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm shiftType :: (LCType, Int) -> LCType module LambdaCube.SystemFw.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.SystemFw.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.SystemFw.TH qTerm :: QuasiQuoter qType :: QuasiQuoter qKind :: QuasiQuoter module LambdaCube.SystemFw.TypeChecker reduceType :: LCType -> LCType infer :: LCTerm -> LCType inferKind :: [LCKind] -> LCType -> LCKind module LambdaCube.SystemFw module LambdaCube.SystemFw_.Ast data ExtLCTerm ExtLCVar :: Text -> ExtLCTerm ExtLCLam :: Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm ExtLCApp :: ExtLCTerm -> ExtLCTerm -> ExtLCTerm ExtLCMVar :: String -> ExtLCTerm infixl 6 `ExtLCApp` data ExtLCType ExtLCBase :: ExtLCType ExtLCTVar :: Text -> ExtLCType ExtLCArr :: ExtLCType -> ExtLCType -> ExtLCType ExtLCTTLam :: Text -> ExtLCKind -> ExtLCType -> ExtLCType ExtLCTTApp :: ExtLCType -> ExtLCType -> ExtLCType ExtLCMTVar :: String -> ExtLCType infixl 6 `ExtLCTTApp` infixr 5 `ExtLCArr` data ExtLCKind ExtLCStar :: ExtLCKind ExtLCKArr :: ExtLCKind -> ExtLCKind -> ExtLCKind ExtLCMKVar :: String -> ExtLCKind infixr 5 `ExtLCKArr` data LCTerm LCVar :: Int -> LCTerm LCLam :: LCType -> LCTerm -> LCTerm LCApp :: LCTerm -> LCTerm -> LCTerm infixl 6 `LCApp` data LCType LCBase :: LCType LCTVar :: Int -> LCType LCArr :: LCType -> LCType -> LCType LCTTLam :: LCKind -> LCType -> LCType LCTTApp :: LCType -> LCType -> LCType infixl 6 `LCTTApp` infixr 5 `LCArr` data LCKind LCStar :: LCKind LCKArr :: LCKind -> LCKind -> LCKind infixr 5 `LCKArr` data LCValue LCValLam :: LCType -> LCTerm -> LCValue data LCNormalTerm LCNormLam :: LCType -> LCNormalTerm -> LCNormalTerm LCNormNeut :: LCNeutralTerm -> LCNormalTerm data LCNeutralTerm LCNeutVar :: Int -> LCNeutralTerm LCNeutApp :: LCNeutralTerm -> LCNormalTerm -> LCNeutralTerm infixl 6 `LCNeutApp` instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.ExtLCKind instance Data.Data.Data LambdaCube.SystemFw_.Ast.ExtLCKind instance GHC.Show.Show LambdaCube.SystemFw_.Ast.ExtLCKind instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.ExtLCKind instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.ExtLCType instance Data.Data.Data LambdaCube.SystemFw_.Ast.ExtLCType instance GHC.Show.Show LambdaCube.SystemFw_.Ast.ExtLCType instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.ExtLCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.ExtLCTerm instance Data.Data.Data LambdaCube.SystemFw_.Ast.ExtLCTerm instance GHC.Show.Show LambdaCube.SystemFw_.Ast.ExtLCTerm instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.ExtLCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.LCKind instance Data.Data.Data LambdaCube.SystemFw_.Ast.LCKind instance GHC.Show.Show LambdaCube.SystemFw_.Ast.LCKind instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.LCKind instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.LCType instance Data.Data.Data LambdaCube.SystemFw_.Ast.LCType instance GHC.Show.Show LambdaCube.SystemFw_.Ast.LCType instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.LCType instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.LCTerm instance Data.Data.Data LambdaCube.SystemFw_.Ast.LCTerm instance GHC.Show.Show LambdaCube.SystemFw_.Ast.LCTerm instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.LCTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.LCValue instance Data.Data.Data LambdaCube.SystemFw_.Ast.LCValue instance GHC.Show.Show LambdaCube.SystemFw_.Ast.LCValue instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.LCValue instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.LCNormalTerm instance Data.Data.Data LambdaCube.SystemFw_.Ast.LCNormalTerm instance GHC.Show.Show LambdaCube.SystemFw_.Ast.LCNormalTerm instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.LCNormalTerm instance Language.Haskell.TH.Syntax.Lift LambdaCube.SystemFw_.Ast.LCNeutralTerm instance Data.Data.Data LambdaCube.SystemFw_.Ast.LCNeutralTerm instance GHC.Show.Show LambdaCube.SystemFw_.Ast.LCNeutralTerm instance GHC.Classes.Eq LambdaCube.SystemFw_.Ast.LCNeutralTerm module LambdaCube.SystemFw_.Elaborator elaborate :: ExtLCTerm -> LCTerm elaborateType :: ExtLCType -> LCType elaborateKind :: ExtLCKind -> LCKind module LambdaCube.SystemFw_.Lifter liftLCValue :: LCValue -> LCTerm liftLCNormal :: LCNormalTerm -> LCTerm module LambdaCube.SystemFw_.Parser pTopTerm :: Parser ExtLCTerm pTopType :: Parser ExtLCType pTopKind :: Parser ExtLCKind module LambdaCube.SystemFw_.PrettyPrinter prettyUnnamedTerm :: LCTerm -> Text prettyShowUnnamedTerm :: LCTerm -> String prettyUnnamedType :: LCType -> Text prettyShowUnnamedType :: LCType -> String prettyUnnamedKind :: LCKind -> Text prettyShowUnnamedKind :: LCKind -> String module LambdaCube.SystemFw_.Substitution substituteTypeInType :: LCType -> Int -> LCType -> LCType substituteValue :: LCValue -> Int -> LCTerm -> LCTerm substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm module LambdaCube.SystemFw_.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.SystemFw_.TH qTerm :: QuasiQuoter qType :: QuasiQuoter qKind :: QuasiQuoter module LambdaCube.SystemFw_.TypeChecker reduceType :: LCType -> LCType infer :: LCTerm -> LCType inferKind :: LCType -> LCKind module LambdaCube.SystemFw_.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.SystemFw_