dedukti-1.0.0: A type-checker for the » -modulo calculus. Source code Contents Index

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 Instances Eq Code Show Code

data Term Source

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 Source

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

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

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

A box in which we didn't put anything.

obj :: Term -> Code Source

start :: IO UTCTime Source

stop :: UTCTime -> IO () Source

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

checkRule :: Term -> Term -> Term Source

Produced by Haddock version 2.4.2