Module ToAgda

A transformation of Curry programs into Agda programs.

Author: Michael Hanus

Version: April 2021

Summary of exported operations:

theoremToAgda :: Options -> (String,String) -> [CFuncDecl] -> [CTypeDecl] -> IO ()  Non-deterministic 
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 ()  Non-deterministic 

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