| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Certifier
Synopsis
- runCertifier ∷ Maybe String → SimplifierTrace Name DefaultUni DefaultFun a → IO ()
Documentation
Arguments
| ∷ Maybe String | Should we run the Agda certifier? If so, what should the certificate file be called? |
| → SimplifierTrace Name DefaultUni DefaultFun a | The trace produced by the simplification process |
| → IO () |
Run the Agda certifier on the simplification trace, if requested