inductive Cedar.Spec.BinaryOp.CanError : BinaryOp → Prop

• add : BinaryOp.add.CanError
• sub : BinaryOp.sub.CanError
• mul : BinaryOp.mul.CanError
• getTag : BinaryOp.getTag.CanError

inductive Cedar.Spec.UnaryOp.CanError : UnaryOp → Prop

• neg : UnaryOp.neg.CanError

inductive Cedar.Spec.Residual.ErrorFree : Residual → Prop

• val {v : Value} {ty : Validation.CedarType} : (Residual.val v ty).ErrorFree
• var {v : Var} {ty : Validation.CedarType} : (Residual.var v ty).ErrorFree
• unary {x₁ : Residual} {op : UnaryOp} {ty : Validation.CedarType} : ¬op.CanError → x₁.ErrorFree → (unaryApp op x₁ ty).ErrorFree
• binary {x₁ x₂ : Residual} {op : BinaryOp} {ty : Validation.CedarType} : ¬op.CanError → x₁.ErrorFree → x₂.ErrorFree → (binaryApp op x₁ x₂ ty).ErrorFree
• and {x₁ x₂ : Residual} {ty : Validation.CedarType} : x₁.ErrorFree → x₂.ErrorFree → (x₁.and x₂ ty).ErrorFree
• or {x₁ x₂ : Residual} {ty : Validation.CedarType} : x₁.ErrorFree → x₂.ErrorFree → (x₁.or x₂ ty).ErrorFree
• ite {x₁ x₂ x₃ : Residual} {ty : Validation.CedarType} : x₁.ErrorFree → x₂.ErrorFree → x₃.ErrorFree → (x₁.ite x₂ x₃ ty).ErrorFree
• hasAttr {x₁ : Residual} {attr : Attr} {ty : Validation.CedarType} : x₁.ErrorFree → (x₁.hasAttr attr ty).ErrorFree
• set {rs : List Residual} {ty : Validation.CedarType} : (∀ (r : Residual), r ∈ rs → r.ErrorFree) → (Residual.set rs ty).ErrorFree
• record {axs : List (Attr × Residual)} {ty : Validation.CedarType} : (∀ (ax : Attr × Residual), ax ∈ axs → ax.snd.ErrorFree) → (Residual.record axs ty).ErrorFree

theorem Cedar.Thm.BinaryOp.can_error_spec (op : Spec.BinaryOp) : op.canError = true ↔ op.CanError

theorem Cedar.Thm.UnaryOp.can_error_spec (op : Spec.UnaryOp) : op.canError = true ↔ op.CanError

@[irreducible]

theorem Cedar.Thm.Residual.error_free_spec (r : Spec.Residual) : r.errorFree = true ↔ r.ErrorFree

@[irreducible]

theorem Cedar.Thm.error_free_evaluate_ok {req : Spec.Request} {es : Spec.Entities} {env : Validation.TypeEnv} {r : Spec.Residual} : InstanceOfWellFormedEnvironment req es env → Residual.WellTyped env r → r.ErrorFree → Except.isOk (r.evaluate req es) = true