mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
ee09768de4
6 files passed under Lean's default but failed under the project's
`autoImplicit := false`: they relied on auto-bound implicits (FunctionalAgent's
α/β/γ/δ; Consensus/{Safety,Liveness} p:Params; Warp/{Ordering,Delivery} s';
Crypto/FROST Share index). Added explicit variable/binder declarations
(declaration-only; no proof meaning changed). Whole lean/ library now verifies
at 0 errors under `lake env lean -D autoImplicit=false` (88/88 files).
Co-authored-by: Hanzo Dev <[email protected]>