| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Coq.Converter.FuncDecl.Rec
Description
This module contains a function for converting mutually recursive Haskell functions to Coq.
Synopsis
- convertRecFuncDecls :: [FuncDecl] -> Converter [Sentence]
Documentation
convertRecFuncDecls :: [FuncDecl] -> Converter [Sentence] Source #
Converts (mutually) recursive Haskell function declarations to Coq.
The function declarations are analyzed first. If they contain constant
arguments (i.e. arguments that are passed unchanged between recursive
calls), they are converted using a Section sentence (see
convertRecFuncDeclsWithHelpers). Otherwise they are converted into
helper and main functions (see convertRecFuncDeclsWithSection).