| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Coq.Converter.FuncDecl.NonRec
Description
This module contains a function for converting non-recursive Haskell functions to Coq.
Synopsis
- convertNonRecFuncDecl :: FuncDecl -> Converter Sentence
- convertNonRecFuncDecls :: [FuncDecl] -> Converter [Sentence]
Documentation
convertNonRecFuncDecl :: FuncDecl -> Converter Sentence Source #
Converts a non-recursive Haskell function declaration to a Coq
Definition sentence.
convertNonRecFuncDecls :: [FuncDecl] -> Converter [Sentence] Source #
Converts non-recursive but possibly linear dependent Haskell functions
into an ordered list of Definition sentences such that each definition
only depends on definitions at preceding list positions.