Lean (version 4.30.0, x86_64-unknown-linux-gnu, commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release)
Source guard: no sorry, admit, or custom axiom declarations.
Checking Fragments.lean
Checking Contexts.lean
'FPRD.Boundary.client_congruence' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.contextualEq_iff_relEq' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.exact_summary_refines_relation' depends on axioms: [propext, Quot.sound]
Checking Adaptive.lean
'FPRD.Boundary.contextualEq_implies_adaptiveEq' does not depend on any axioms
'FPRD.Boundary.adaptiveEq_iff_relEq' depends on axioms: [propext, Quot.sound]
Checking Summaries.lean
'FPRD.Boundary.decodeSummary_correct' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.exactSummary_iff_decoder' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.unequal_relations_force_distinct_summaries' depends on axioms: [propext, Quot.sound]
Checking Examples.lean
'FPRD.Boundary.Examples.fresh_private_join_sat' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Examples.distinct_private_syntax_same_future' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Examples.aliased_private_unsat' depends on axioms: [propext]
'FPRD.Boundary.Examples.both_sat_but_not_contextualEq' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Examples.positive_clients_cannot_separate' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Examples.forgotten_name_not_reexposed' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Examples.original_name_cannot_be_false' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.finite_boundary_contextualEq_iff_relEq' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.finite_boundary_adaptiveEq_iff_relEq' depends on axioms: [propext, Quot.sound]
Checking Audit.lean
'FPRD.Boundary.PrivateShape.mem_enumerate' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Fragment.rel_join' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Fragment.rel_introduce' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Fragment.rel_forget' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Fragment.rel_renameBoundary' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Fragment.rel_renamePrivate' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.Fragment.rel_pin' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.client_congruence' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.sat_pinAll' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.contextualEq_iff_boundary_eq' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.finite_boundary_contextualEq_iff_relEq' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.finite_boundary_adaptiveEq_iff_relEq' depends on axioms: [propext, Quot.sound]
'FPRD.Boundary.exactSummary_iff_decoder' depends on axioms: [propext, Quot.sound]
All required source modules passed Lean kernel checking.
