Dedukti.Runtime

All generated Haskell files import this module. The data type declarations are given here, along with the conversion relation and type inference function.

Documentation

data Code

Constructors

Var !Int

Con !ByteString

Lam !(Code -> Code)

Pi Code !(Code -> Code)

App Code Code

Type

Kind

Instances

Eq Code

Show Code

Pretty Code

Eq (Code -> Code)

data Term

Constructors

TLam !Term !(Term -> Term)

TPi !Term !(Term -> Term)

TApp !Term !Term

TType

Box Code Code

UBox Term Code

Instances

Show Term

ap :: Code -> Code -> Code

convertible :: Int -> Code -> Code -> Bool

bbox :: Term -> Code -> Code -> Term

sbox :: Term -> Code -> Code -> Term

A box in which we didn't put anything.

obj :: Term -> Code

start :: IO UTCTime

stop :: UTCTime -> IO ()

checkDeclaration :: String -> Term -> IO ()

checkRule :: Term -> Term -> Term