| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Certifier
Synopsis
- runCertifier ∷ Certifier a → IO (Either CertifierError a)
- mkCertifier ∷ SimplifierTrace Name DefaultUni DefaultFun a → CertName → Certifier CertifierSuccess
- prettyCertifierError ∷ CertifierError → String
- prettyCertifierSuccess ∷ CertifierSuccess → String
- data CertifierError
- = InvalidCertificate CertDir
- | InvalidCompilerOutput
- | ValidationError CertName
Documentation
runCertifier ∷ Certifier a → IO (Either CertifierError a) Source #
Arguments
| ∷ SimplifierTrace Name DefaultUni DefaultFun a | The trace produced by the simplification process |
| → CertName | The name of the certificate to be produced |
| → Certifier CertifierSuccess |
Run the Agda certifier on the simplification trace, if requested
prettyCertifierSuccess ∷ CertifierSuccess → String Source #
data CertifierError Source #
Constructors
| InvalidCertificate CertDir | |
| InvalidCompilerOutput | |
| ValidationError CertName |