-- 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.2.0.0 module LambdaCube.Common.Parser type Parser = Parsec Void Text topParser :: Parser a -> Parser a parenthesized :: Parser a -> Parser a 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 identifier :: Parser Text lex :: Parser a -> Parser a module LambdaCube.Common.PrettyPrinter wrapIfSpaced :: Bool -> [Text] -> Text wrap :: Text -> Text wrapIf :: Bool -> Text -> Text spaced :: [Text] -> Text module LambdaCube.STLC.Ast data ExtLCType ExtLCBase :: ExtLCType ExtLCArr :: ExtLCType -> ExtLCType -> ExtLCType ExtLCMTVar :: String -> ExtLCType infixr 5 `ExtLCArr` data ExtLCTerm ExtLCVar :: Text -> ExtLCTerm ExtLCLam :: Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm ExtLCApp :: ExtLCTerm -> ExtLCTerm -> ExtLCTerm ExtLCMVar :: String -> ExtLCTerm infixl 6 `ExtLCApp` data LCType LCBase :: LCType LCArr :: LCType -> LCType -> LCType infixr 5 `LCArr` data LCTerm LCVar :: Int -> LCTerm LCLam :: LCType -> LCTerm -> LCTerm LCApp :: LCTerm -> LCTerm -> LCTerm infixl 6 `LCApp` 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 elaborateType :: ExtLCType -> LCType elaborate :: ExtLCTerm -> LCTerm module LambdaCube.STLC.Lifter liftLCValue :: LCValue -> LCTerm liftLCNormal :: LCNormalTerm -> LCTerm liftLCNeutral :: LCNeutralTerm -> LCTerm module LambdaCube.STLC.Parser pTopLC :: Parser ExtLCTerm pLC :: Parser ExtLCTerm pLam :: Parser ExtLCTerm pApp :: Parser ExtLCTerm pATerm :: Parser ExtLCTerm pVar :: Parser ExtLCTerm pMVar :: Parser ExtLCTerm pType :: Parser ExtLCType pAType :: Parser ExtLCType pBase :: Parser ExtLCType pMTVar :: Parser ExtLCType module LambdaCube.STLC.PrettyPrinter prettyUnnamedType :: LCType -> Text prettyUnnamedTerm :: LCTerm -> Text prettyUnnamedTypePrec :: Int -> LCType -> Text prettyUnnamedTermPrec :: Int -> LCTerm -> Text module LambdaCube.STLC.Substitution substituteValue :: Int -> LCValue -> LCTerm -> LCTerm substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm module LambdaCube.STLC.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.STLC.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.STLC.TH lc :: QuasiQuoter module LambdaCube.STLC.TypeChecker infer :: LCTerm -> LCType module LambdaCube.STLC module LambdaCube.SystemF.Ast data ExtLCType ExtLCBase :: ExtLCType ExtLCTVar :: Text -> ExtLCType ExtLCArr :: ExtLCType -> ExtLCType -> ExtLCType ExtLCUniv :: Text -> ExtLCType -> ExtLCType ExtLCMTVar :: String -> ExtLCType infixr 5 `ExtLCArr` 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 LCType LCBase :: LCType LCTVar :: Int -> LCType LCArr :: LCType -> LCType -> LCType LCUniv :: LCType -> LCType infixr 5 `LCArr` 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 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 liftLCNeutral :: LCNeutralTerm -> LCTerm module LambdaCube.SystemF.Parser pTopLC :: Parser ExtLCTerm pLC :: Parser ExtLCTerm pTLam :: Parser ExtLCTerm pLam :: Parser ExtLCTerm pApp :: Parser ExtLCTerm pAppArg :: Parser (ExtLCTerm -> ExtLCTerm) pATerm :: Parser ExtLCTerm pVar :: Parser ExtLCTerm pMVar :: Parser ExtLCTerm pType :: Parser ExtLCType pUniv :: Parser ExtLCType pArr :: Parser ExtLCType pAType :: Parser ExtLCType pBase :: Parser ExtLCType pTVar :: Parser ExtLCType pMTVar :: Parser ExtLCType module LambdaCube.SystemF.PrettyPrinter prettyUnnamedType :: LCType -> Text prettyUnnamedTerm :: LCTerm -> Text prettyUnnamedTypePrec :: Int -> LCType -> Text prettyUnnamedTermPrec :: Int -> LCTerm -> Text module LambdaCube.SystemF.Substitution substituteType :: Int -> LCType -> LCTerm -> LCTerm substituteTypeInType :: Int -> LCType -> LCType -> LCType substituteValue :: Int -> LCValue -> LCTerm -> LCTerm substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm module LambdaCube.SystemF.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.SystemF.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.SystemF.TH lc :: QuasiQuoter module LambdaCube.SystemF.TypeChecker infer :: LCTerm -> LCType module LambdaCube.SystemF module LambdaCube.SystemFw.Ast data ExtLCKind ExtLCStar :: ExtLCKind ExtLCKArr :: ExtLCKind -> ExtLCKind -> ExtLCKind ExtLCMKVar :: String -> ExtLCKind infixr 5 `ExtLCKArr` 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 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 LCKind LCStar :: LCKind LCKArr :: LCKind -> LCKind -> LCKind infixr 5 `LCKArr` 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 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 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 liftLCNeutral :: LCNeutralTerm -> LCTerm module LambdaCube.SystemFw.Parser pTopLC :: Parser ExtLCTerm pLC :: Parser ExtLCTerm pTLam :: Parser ExtLCTerm pLam :: Parser ExtLCTerm pApp :: Parser ExtLCTerm pAppArg :: Parser (ExtLCTerm -> ExtLCTerm) pATerm :: Parser ExtLCTerm pVar :: Parser ExtLCTerm pMVar :: Parser ExtLCTerm pType :: Parser ExtLCType pTTLam :: Parser ExtLCType pUniv :: Parser ExtLCType pArr :: Parser ExtLCType pTTApp :: Parser ExtLCType pAType :: Parser ExtLCType pBase :: Parser ExtLCType pTVar :: Parser ExtLCType pMTVar :: Parser ExtLCType pKind :: Parser ExtLCKind pAKind :: Parser ExtLCKind pStar :: Parser ExtLCKind pMKVar :: Parser ExtLCKind module LambdaCube.SystemFw.PrettyPrinter prettyUnnamedKind :: LCKind -> Text prettyUnnamedType :: LCType -> Text prettyUnnamedTerm :: LCTerm -> Text prettyUnnamedKindPrec :: Int -> LCKind -> Text prettyUnnamedTypePrec :: Int -> LCType -> Text prettyUnnamedTermPrec :: Int -> LCTerm -> Text module LambdaCube.SystemFw.Substitution substituteType :: Int -> LCType -> LCTerm -> LCTerm substituteTypeInType :: Int -> LCType -> LCType -> LCType substituteValue :: Int -> LCValue -> LCTerm -> LCTerm substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm module LambdaCube.SystemFw.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.SystemFw.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.SystemFw.TH lc :: QuasiQuoter module LambdaCube.SystemFw.TypeChecker reduceType :: LCType -> LCType infer :: LCTerm -> LCType inferKind :: LCType -> LCKind module LambdaCube.SystemFw module LambdaCube.SystemFw_.Ast data ExtLCKind ExtLCStar :: ExtLCKind ExtLCKArr :: ExtLCKind -> ExtLCKind -> ExtLCKind ExtLCMKVar :: String -> ExtLCKind infixr 5 `ExtLCKArr` 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 ExtLCTerm ExtLCVar :: Text -> ExtLCTerm ExtLCLam :: Text -> ExtLCType -> ExtLCTerm -> ExtLCTerm ExtLCApp :: ExtLCTerm -> ExtLCTerm -> ExtLCTerm ExtLCMVar :: String -> ExtLCTerm infixl 6 `ExtLCApp` data LCKind LCStar :: LCKind LCKArr :: LCKind -> LCKind -> LCKind infixr 5 `LCKArr` 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 LCTerm LCVar :: Int -> LCTerm LCLam :: LCType -> LCTerm -> LCTerm LCApp :: LCTerm -> LCTerm -> LCTerm infixl 6 `LCApp` 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 liftLCNeutral :: LCNeutralTerm -> LCTerm module LambdaCube.SystemFw_.Parser pTopLC :: Parser ExtLCTerm pLC :: Parser ExtLCTerm pLam :: Parser ExtLCTerm pApp :: Parser ExtLCTerm pATerm :: Parser ExtLCTerm pVar :: Parser ExtLCTerm pMVar :: Parser ExtLCTerm pType :: Parser ExtLCType pTTLam :: Parser ExtLCType pArr :: Parser ExtLCType pTTApp :: Parser ExtLCType pAType :: Parser ExtLCType pBase :: Parser ExtLCType pTVar :: Parser ExtLCType pMTVar :: Parser ExtLCType pKind :: Parser ExtLCKind pAKind :: Parser ExtLCKind pStar :: Parser ExtLCKind pMKVar :: Parser ExtLCKind module LambdaCube.SystemFw_.PrettyPrinter prettyUnnamedKind :: LCKind -> Text prettyUnnamedType :: LCType -> Text prettyUnnamedTerm :: LCTerm -> Text prettyUnnamedKindPrec :: Int -> LCKind -> Text prettyUnnamedTypePrec :: Int -> LCType -> Text prettyUnnamedTermPrec :: Int -> LCTerm -> Text module LambdaCube.SystemFw_.Substitution substituteTypeInType :: Int -> LCType -> LCType -> LCType substituteValue :: Int -> LCValue -> LCTerm -> LCTerm substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm module LambdaCube.SystemFw_.Evaluator evaluate :: LCTerm -> LCValue module LambdaCube.SystemFw_.TH lc :: QuasiQuoter module LambdaCube.SystemFw_.TypeChecker reduceType :: LCType -> LCType infer :: LCTerm -> LCType inferKind :: LCType -> LCKind module LambdaCube.SystemFw_.Normalizer normalize :: LCTerm -> LCNormalTerm module LambdaCube.SystemFw_