This file defines the Result type for symbolic compilation.

inductive Cedar.SymCC.Error : Type

• noSuchEntityType : Error
• noSuchAttribute : Error
• typeError : Error
• unsupportedError : Error

@[reducible, inline]

abbrev Cedar.SymCC.Result (α : Type u_1) : Type u_1

Equations

• Cedar.SymCC.Result α = Except Cedar.SymCC.Error α

instance Cedar.SymCC.instReprError : Repr Error

Equations

• Cedar.SymCC.instReprError = { reprPrec := Cedar.SymCC.instReprError.repr }

def Cedar.SymCC.instReprError.repr : Error → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.instReprError.repr Cedar.SymCC.Error.typeError prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Error.typeError")).group prec✝

instance Cedar.SymCC.instDecidableEqError : DecidableEq Error

Equations

• Cedar.SymCC.instDecidableEqError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cedar.SymCC.instInhabitedError.default : Error

Equations

• Cedar.SymCC.instInhabitedError.default = Cedar.SymCC.Error.noSuchEntityType

instance Cedar.SymCC.instInhabitedError : Inhabited Error

Equations

• Cedar.SymCC.instInhabitedError = { default := Cedar.SymCC.instInhabitedError.default }

@[inline]

instance Cedar.SymCC.coeResult {α : Type u_1} : Coe α (Result α)

Equations

• Cedar.SymCC.coeResult = { coe := fun (a : α) => Except.ok a }

instance Cedar.SymCC.instToStringError : ToString Error

Equations

• One or more equations did not get rendered due to their size.