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

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_reducible]

instance Cedar.Spec.instReprDecision : Repr Decision

Equations

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

@[instance_reducible]

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.instReprResponse.repr : Response → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cedar.Spec.instReprResponse : Repr Response

Equations

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

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_reducible]

instance Cedar.Spec.instDecidableEqResponse : DecidableEq Response

Equations

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