This file defines Cedar responses.

inductive Cedar.Spec.Decision : Type

• allow : Decision
• deny : Decision

structure Cedar.Spec.Response : Type

• decision : Decision
• determiningPolicies : Data.Set PolicyID
• erroringPolicies : Data.Set PolicyID

instance Cedar.Spec.instReprDecision : Repr Decision

Equations

• Cedar.Spec.instReprDecision = { reprPrec := Cedar.Spec.instReprDecision.repr }

def Cedar.Spec.instReprDecision.repr : Decision → Nat → Std.Format

Equations

• Cedar.Spec.instReprDecision.repr Cedar.Spec.Decision.allow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Decision.allow")).group prec✝
• Cedar.Spec.instReprDecision.repr Cedar.Spec.Decision.deny prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Decision.deny")).group prec✝

instance Cedar.Spec.instDecidableEqDecision : DecidableEq Decision

Equations

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

def Cedar.Spec.instToJsonDecision.toJson : Decision → Lean.Json

Equations

• Cedar.Spec.instToJsonDecision.toJson Cedar.Spec.Decision.allow = Lean.toJson "allow"
• Cedar.Spec.instToJsonDecision.toJson Cedar.Spec.Decision.deny = Lean.toJson "deny"

instance Cedar.Spec.instToJsonDecision : Lean.ToJson Decision

Equations

• Cedar.Spec.instToJsonDecision = { toJson := Cedar.Spec.instToJsonDecision.toJson }

instance Cedar.Spec.instReprResponse : Repr Response

Equations

• Cedar.Spec.instReprResponse = { reprPrec := Cedar.Spec.instReprResponse.repr }

def Cedar.Spec.instReprResponse.repr : Response → Nat → Std.Format

Equations

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

def Cedar.Spec.instDecidableEqResponse.decEq (x✝ x✝¹ : Response) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.Spec.instDecidableEqResponse : DecidableEq Response

Equations

• Cedar.Spec.instDecidableEqResponse = Cedar.Spec.instDecidableEqResponse.decEq

instance Cedar.Spec.instToJsonResponse : Lean.ToJson Response

Equations

• Cedar.Spec.instToJsonResponse = { toJson := Cedar.Spec.instToJsonResponse.toJson }

def Cedar.Spec.instToJsonResponse.toJson : Response → Lean.Json

Equations

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