allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: eliminate cross-project Semantics.FixedPoint imports

Browse source 
Schema.lean and Receipt.lean now import SilverSight.FixedPoint
instead of Semantics.FixedPoint. SilverSight builds standalone.

Build: 3307 jobs, 0 errors.
This commit is contained in:
allaun 2026-06-23 05:56:27 -05:00
parent a783a15750
commit 8fd4638240
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
formal/SilverSight/Receipt.lean
View file

@ -1,9 +1,9 @@
import Semantics.FixedPoint
import SilverSight.FixedPoint
namespace SilverSight
open Semantics.FixedPoint
open Semantics.FixedPoint.Q16_16
open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16
-- ═══════════════════════════════════════════════════════════════════════════
-- §1 Gate types

4
formal/SilverSight/Schema.lean
View file

@ -1,8 +1,8 @@
import Semantics.FixedPoint
import SilverSight.FixedPoint
namespace SilverSight
open Semantics.FixedPoint
open SilverSight.FixedPoint
/-- A Schema describes the wire-level layout of a type:
- `byteSize`: the number of bytes in the wire representation