Research source · Plain text

Audit.lean

site/public/formal/boundary-context/Audit.lean

18 lines. Source is displayed for inspection; it is not executed by this page.

File fingerprint

SHA-256: d34ab9d99efe06d4d353e4831cb44379254708599ff8a3c5ebe23fb262069cd1

import Examples
import Summaries

namespace FPRD.Boundary
#print axioms PrivateShape.mem_enumerate
#print axioms Fragment.rel_join
#print axioms Fragment.rel_introduce
#print axioms Fragment.rel_forget
#print axioms Fragment.rel_renameBoundary
#print axioms Fragment.rel_renamePrivate
#print axioms Fragment.rel_pin
#print axioms client_congruence
#print axioms sat_pinAll
#print axioms contextualEq_iff_boundary_eq
#print axioms finite_boundary_contextualEq_iff_relEq
#print axioms finite_boundary_adaptiveEq_iff_relEq
#print axioms exactSummary_iff_decoder
end FPRD.Boundary