Module ToAgda

Exported Functions

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.