| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Certifier
Synopsis
- runCertifier :: Certifier a -> DefaultFun a
The trace produced by the simplification process
-> CertName The name of the certificate to be produced
-> CertifierOutput -> Certifier Bool
Run the Agda certifier on the simplification trace, if requested