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 11 research declarations. Search 10,000 more complete Mathlib declarations.
11 results
Clear filtersCedar.Thm.wellTypedPolicy_preserves_valid_refs
Plain-language statement
wellTypedPolicy preserves Entities.ValidRefsFor.
Source project: Cedar Specification
Person-level attribution pending.
compile_binaryApp_wf_types
Plain-language statement
Similar to compileApp₂_wf_types, but for compile
Source project: Cedar Specification
Person-level attribution pending.
compile_ok_implies_compile_well_typed_binaryApp
Project documentation
Since we have the nice lemma compileApp₂_wf_types, it's enough to prove that compile of a binaryApp succeeds.
Source project: Cedar Specification
Person-level attribution pending.
compile_well_typed_on_wf_expr
Plain-language statement
Compiling a well-typed expression should produce a term of the corresponding TermType, assuming that the expression is well-formed in the symbolic environment.
Source project: Cedar Specification
Person-level attribution pending.
compile_well_typed_or_and
Plain-language statement
Combined case for or and and
Source project: Cedar Specification
Person-level attribution pending.