| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Certifier
Synopsis
- runCertifier ∷ Certifier a → IO (Either CertifierError a)
- mkCertifier ∷ SimplifierTrace Name DefaultUni DefaultFun a → CertName → CertifierOutput → Certifier ()
- prettyCertifierError ∷ CertifierError → String
- data CertifierError
- = InvalidCertificate CertDir
- | InvalidCompilerOutput
- | ValidationError CertName
- data CertifierOutput
- = BasicOutput
- | ReportOutput FilePath
- | ProjectOutput CertDir
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 |
| → CertifierOutput | |
| → Certifier () |
Run the Agda certifier on the simplification trace, if requested
data CertifierError Source #
Constructors
| InvalidCertificate CertDir | |
| InvalidCompilerOutput | |
| ValidationError CertName |
data CertifierOutput Source #
Constructors
| BasicOutput | Print minimal basic info, such as "passed" or "failed" |
| ReportOutput FilePath | Produce a detailed human readable report |
| ProjectOutput CertDir | Produce an Agda project that can be type checked |