Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 200 research declarations. Search 10,000 more complete Mathlib declarations.
200 results
Clear filtersCedar.Thm.cpset_satAssertsOpt?_eqv_satAsserts?_ok
Project documentation
This theorem covers the "happy path" -- showing that if optimized policy compilation with CompiledPolicySet.compile succeeds, then satAsserts? and satAssertsOpt? are equivalent.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.default_lit_wf
Plain-language statement
Decoder.defaultLit is well-formed if given sufficiently well-formed eidOf and ty.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.denied_iff_explicitly_denied_or_not_permitted
Plain-language statement
A request is denied if and only if it is explicitly denied or it is not explicitly permitted.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.determining_erroring_disjoint_when_unique_ids
Plain-language statement
Determining policies and erroring policies of an isAuthorized response are disjoint when input policy IDs are unique.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.disjointOpt?_eqv_disjoint?
Plain-language statement
Full equivalence for disjoint? and disjointOpt?, including both the .ok and .error cases
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.disjointOpt?_eqv_disjoint?_ok
Project documentation
This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicies succeeds and disjoint? and disjointOpt? are equivalent.
Source project: Cedar Specification
Person-level attribution pending.