| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Coq.Converter.FuncDecl.Common
Contents
Description
This module contains auxiliary functions that are used to translate both recursive and non-recursive Haskell functions to Coq.
Synopsis
- convertFuncHead :: FuncDecl -> Converter (Qualid, [Binder], Maybe Term)
Code Generation
convertFuncHead :: FuncDecl -> Converter (Qualid, [Binder], Maybe Term) Source #
Converts the name, arguments and return type of a function to Coq.
This code is shared between the conversion functions for recursive and
no recursive functions
(see convertNonRecFuncDecl
and convertRecFuncDecls).