Sync from GitHub AHMADALIPARR/cpsc-qft@2603e23: axiom-free Operator.lean, axiom audit
5736180 verified | /- | |
| Copyright (c) 2026 Ahmad Ali Parr and others. | |
| SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only | |
| -/ | |
| import CPSC.Certificate | |
| import CPSC.Operator | |
| import CPSC.Lemmas | |
| import CPSC.Emitted | |