Inner Signature summary
|
signature BASE_PRETTY_PRINTER
The First-Order LoopW Proof Checker base pretty-printer.
|
signature COMPILER
The First-Order LoopW Proof Checker compiler.
|
signature FUN_PRETTY_PRINTER
The First-Order LoopW Proof Checker functional pretty-printer.
|
signature FUN_TRANSLATION
The First-Order LoopW Proof Checker translator into functional syntax.
|
signature LIST_ASSOC
Utility functions that deals with association lists.
|
signature PRETTY_PRINTER_KEYWORDS
The First-Order LoopW Proof Checker pretty-printer keywords for abstract syntax.
|
signature PROOF_AST_UTILS
Utility function for the proof syntax.
|
signature PROOF_CHECKER
The First-Order LoopW Proof Checker proof checking.
|
signature PROOF_ENVIRONMENT
The First-Order LoopW Proof Checker proof environment abstract type.
|
signature PROOF_PRETTY_PRINTER
The First-Order LoopW Proof Checker proof syntax pretty-printer.
|
signature TERMS
The First-Order LoopW Proof Checker formula/term substitution and alpha-equivalence.
|
signature UTILS
Utility functions that deals with lists.
|
Inner Structure summary
|
structure BasePrettyPrinter
The First-Order LoopW Proof Checker base pretty-printer.
|
structure Compiler
The First-Order LoopW Proof Checker compiler.
|
structure Error
The First-Order LoopW Proof Checker syntax error module.
|
structure FunAst
The First-Order LoopW Proof Checker functional programs abstract syntax.
|
structure FunPrettyPrinter
The First-Order LoopW Proof Checker functional pretty-printer.
|
structure FunTranslation
The First-Order LoopW Proof Checker translator into functional syntax.
|
structure FunTypeChecker
|
structure ListAssoc
Utility functions that deals with association lists.
|
structure Main
The First-Order LoopW Proof Checker main program.
|
structure Parser
|
structure PrettyPrinterKeywords
The First-Order LoopW Proof Checker pretty-printer keywords for abstract syntax.
|
structure ProofAst
The First-Order LoopW Proof Checker proof abstract syntax.
|
structure ProofAstUtils
Utility function for the proof syntax.
|
structure ProofChecker
The First-Order LoopW Proof Checker proof checking.
|
structure ProofEnvironment
The First-Order LoopW Proof Checker proof environment abstract type.
|
structure ProofPrettyPrinter
The First-Order LoopW Proof Checker proof syntax pretty-printer.
|
structure Terms
The First-Order LoopW Proof Checker formula/term substitution and alpha-equivalence.
|
structure Utils
Utility functions that deals with lists.
|