Module ToAgda

A transformation of Curry programs into Agda programs.

Author: Michael Hanus

Version: October 2016

Summary of exported operations:

theoremToAgda :: Options -> (String,String) -> [CFuncDecl] -> [CTypeDecl] -> IO ()   
Generate an Agda program file for a given theorem name and the list of all functions involved in this theorem.

Exported operations:

theoremToAgda :: Options -> (String,String) -> [CFuncDecl] -> [CTypeDecl] -> IO ()   

Generate an Agda program file for a given theorem name and the list of all functions involved in this theorem.