A transformation of Curry programs into Agda programs.
Author: Michael Hanus
Version: August 2016
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. |
Generate an Agda program file for a given theorem name and the list of all functions involved in this theorem. |