def Cedar.SymCC.Opt.compileWithEffect (effect : Spec.Effect) (policy : Spec.Policy) (εnv : SymEnv) : Result (Option CompileResult)

Equations

• Cedar.SymCC.Opt.compileWithEffect effect policy εnv = if (policy.effect == effect) = true then do let a ← Cedar.SymCC.Opt.compile policy.toExpr εnv pure (some a) else Except.ok none

def Cedar.SymCC.Opt.satisfiedPolicies (effect : Spec.Effect) (policies : Spec.Policies) (εnv : SymEnv) : Result CompileResult

Equations

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

def Cedar.SymCC.Opt.isAuthorized (policies : Spec.Policies) (εnv : SymEnv) : Result CompileResult

Equations

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