Documentation

LeanCert.Engine.Eval.Result

Checked evaluation results #

Certified evaluators return a finite enclosure only after all partial-domain conditions have been checked. Failures are data: callers must propagate them instead of substituting a finite sentinel that could be mistaken for an enclosure.

source
inductive LeanCert.Engine.EvalError :
Type

Why a checked evaluator could not produce a finite certified enclosure.

Instances For
    source
    @[instance_reducible]
    instance LeanCert.Engine.instReprEvalError :
    Repr EvalError
    Equations
    source
    def LeanCert.Engine.instReprEvalError.repr :
    EvalError → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LeanCert.Engine.instDecidableEqEvalError.decEq (x✝ x✝¹ : EvalError) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[instance_reducible]
        instance LeanCert.Engine.instDecidableEqEvalError :
        DecidableEq EvalError
        Equations
        source
        @[reducible, inline]
        abbrev LeanCert.Engine.EvalResult (α : Type) :
        Type

        Result type used by checked evaluators and public computation APIs.

        Equations
        Instances For