dedukti-1.0.1: A type-checker for the » -modulo calculus.Source codeContentsIndex
Dedukti.Runtime
Description
All generated Haskell files import this module. The data type declarations are given here, along with the conversion relation and type inference function.
Synopsis
data Code
= Var !Int
| Con !ByteString
| Lam !(Code -> Code)
| Pi Code !(Code -> Code)
| App Code Code
| Type
| Kind
data Term
= TLam !Term !(Term -> Term)
| TPi !Term !(Term -> Term)
| TApp !Term !Term
| TType
| Box Code Code
| UBox Term Code
ap :: Code -> Code -> Code
convertible :: Int -> Code -> Code -> Bool
bbox :: Term -> Code -> Code -> Term
sbox :: Term -> Code -> Code -> Term
obj :: Term -> Code
start :: IO UTCTime
stop :: UTCTime -> IO ()
checkDeclaration :: String -> Term -> IO ()
checkRule :: Term -> Term -> Term
Documentation
data Code Source
Constructors
Var !Int
Con !ByteString
Lam !(Code -> Code)
Pi Code !(Code -> Code)
App Code Code
Type
Kind
show/hide Instances
data Term Source
Constructors
TLam !Term !(Term -> Term)
TPi !Term !(Term -> Term)
TApp !Term !Term
TType
Box Code Code
UBox Term Code
show/hide Instances
ap :: Code -> Code -> CodeSource
convertible :: Int -> Code -> Code -> BoolSource
bbox :: Term -> Code -> Code -> TermSource
sbox :: Term -> Code -> Code -> TermSource
A box in which we didn't put anything.
obj :: Term -> CodeSource
start :: IO UTCTimeSource
stop :: UTCTime -> IO ()Source
checkDeclaration :: String -> Term -> IO ()Source
checkRule :: Term -> Term -> TermSource
Produced by Haddock version 2.4.2