Inner Signature summary
|
signature BASE_PRETTY_PRINTER
The First-Order LoopW Type Inference base pretty-printer.
|
signature COMPILER
The First-Order LoopW Type Inference compiler.
|
signature CORE_AST_UTILS
Utility function for the core syntax.
|
signature CORE_PRETTY_PRINTER
The First-Order LoopW Type Inference core syntax pretty-printer.
|
signature LIST_ASSOC
Utility functions that deals with association lists.
|
signature PRETTY_PRINTER_KEYWORDS
The First-Order LoopW Type Inference pretty-printer keywords for abstract syntax.
|
signature PROOF_DERIV_PRETTY_PRINTER
The First-Order LoopW Type Inference proof derivation pretty-printer.
|
signature PROOF_ENVIRONMENT
The First-Order LoopW Type Inference proof environment abstract type.
|
signature PROOF_INFER
The First-Order LoopW Type Inference proof inference.
|
signature PROOF_PRETTY_PRINTER
The First-Order LoopW Type Inference proof syntax pretty-printer.
|
signature TERMS
The First-Order LoopW Type Inference formula/term substitution and alpha-equivalence.
|
signature TERM_MATCH_UNIF
The First-Order LoopW Type Inference formula/term matching and unification.
|
signature UTILS
Utility functions that deals with lists.
|
Inner Structure summary
|
structure BasePrettyPrinter
The First-Order LoopW Type Inference base pretty-printer.
|
structure Compiler
The First-Order LoopW Type Inference compiler.
|
structure CoreAst
The First-Order LoopW Type Inference core abstract syntax.
|
structure CoreAstUtils
Utility function for the core syntax.
|
structure CorePrettyPrinter
The First-Order LoopW Type Inference core syntax pretty-printer.
|
structure Error
The First-Order LoopW Type Inference syntax error module.
|
structure ListAssoc
Utility functions that deals with association lists.
|
structure Main
The First-Order LoopW Type Inference main program.
|
structure Parser
|
structure PrettyPrinterKeywords
The First-Order LoopW Type Inference pretty-printer keywords for abstract syntax.
|
structure ProofAst
The First-Order LoopW Type Inference proof abstract syntax.
|
structure ProofDerivPrettyPrinter
The First-Order LoopW Type Inference proof derivation pretty-printer.
|
structure ProofEnvironment
The First-Order LoopW Type Inference proof environment abstract type.
|
structure ProofInfer
The First-Order LoopW Type Inference proof inference.
|
structure ProofPrettyPrinter
The First-Order LoopW Type Inference proof syntax pretty-printer.
|
structure TermMatchUnif
The First-Order LoopW Type Inference formula/term matching and unification.
|
structure Terms
The First-Order LoopW Type Inference formula/term substitution and alpha-equivalence.
|
structure Utils
Utility functions that deals with lists.
|