hs-to-coq

Contents:

• Installation
  • Latest release
  • Development version
  • Coq Requirements
  • Test your hs-to-coq installation
  • Troubleshooting
• Quickstart
  • Translating a single Haskell file
  • Local Edit files
  • Additional Coq definitions
  • Strict vs. permissive translation
  • Proofs
  • Translating a multi-file project
  • Avoiding base
• Edit Files
  • General format of edit files
  • Skipping Haskell
  • Adding Coq Commands
  • Renaming and Rewriting
  • Extra information
  • Termination edits
  • Mutual recursion edits
  • Invariant Edit
  • Meta-edits
  • Deprecated edits
• Identifiers and Notation
  • Coq keywords
  • Operators
  • Notation
  • String Notation
• Interface files

Indices and tables

• Index
• Module Index
• Search Page