mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-06 19:25:46 +00:00
allaun
d2eb6a74c4
Some checks are pending
Anti-Smuggle Gate / gate (push) Waiting to run
AVM ISA Cross-Port CI / python (push) Waiting to run
AVM ISA Cross-Port CI / go (push) Waiting to run
AVM ISA Cross-Port CI / rust (push) Waiting to run
AVM ISA Cross-Port CI / c (push) Waiting to run
AVM ISA Cross-Port CI / cpp (push) Waiting to run
AVM ISA Cross-Port CI / julia (push) Waiting to run
AVM ISA Cross-Port CI / r (push) Waiting to run
AVM ISA Cross-Port CI / wolfram-verify (push) Waiting to run
AVM ISA Cross-Port CI / cross-verify (push) Blocked by required conditions
Doc Sync Check / check (push) Waiting to run
Lean Check / build (push) Waiting to run
Python Check / test (push) Waiting to run
Q16_16 Roundtrip / roundtrip (push) Waiting to run
Removed: - @[simp] from 4 conditional lemmas (hypotheses simp can't discharge) - claimBoundary/bridgeNote String defs (dead code in API) - 'expected to be' header wording Added: - isSaturated_or_isActive, isSaturated_iff_not_isActive theorems - primesUpTo edge-case note - cleaner doc wording throughout Kept: - @[simp] on C_finite_zero_eq_one (unconditional, useful) |
||
|---|---|---|
| .. | ||
| BindingSite | ||
| CoreFormalism | ||
| RRCLib | ||
| SilverSight | ||