This file defines Cedar requests.

structure Cedar.Spec.Request : Type

• principal : EntityUID
• action : EntityUID
• resource : EntityUID
• context : Data.Map Attr Value

instance Cedar.Spec.instReprRequest : Repr Request

Equations

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

def Cedar.Spec.instReprRequest.repr : Request → Nat → Std.Format

Equations

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

instance Cedar.Spec.instDecidableEqRequest : DecidableEq Request

Equations

• Cedar.Spec.instDecidableEqRequest = Cedar.Spec.instDecidableEqRequest.decEq

def Cedar.Spec.instDecidableEqRequest.decEq (x✝ x✝¹ : Request) : Decidable (x✝ = x✝¹)

Equations

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

def Cedar.Spec.instInhabitedRequest.default : Request

Equations

• Cedar.Spec.instInhabitedRequest.default = { principal := default, action := default, resource := default, context := default }

instance Cedar.Spec.instInhabitedRequest : Inhabited Request

Equations

• Cedar.Spec.instInhabitedRequest = { default := Cedar.Spec.instInhabitedRequest.default }