Overview  Index  Help 

First-Order LoopW

 
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.

   
Inner Functor summary

functor SyntaxLexFun

         

         


Overview  Index  Help