| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Coq.Converter.FuncDecl
Description
This module contains functions for generating Coq function declarations
(in the form of Definition, Fixpoint and Section sentences) from
our intermediate representation.
Synopsis
- convertFuncDecls :: [FuncDecl] -> Converter [Sentence]
- convertFuncComponent :: DependencyComponent FuncDecl -> Converter [Sentence]
Documentation
convertFuncDecls :: [FuncDecl] -> Converter [Sentence] Source #
Converts the given function declarations.
convertFuncComponent :: DependencyComponent FuncDecl -> Converter [Sentence] Source #
Converts a strongly connected component of the function dependency graph.