From 22782776a90c6b9c2b782b01e61fab82cb59c6f5 Mon Sep 17 00:00:00 2001 From: allaun Date: Mon, 22 Jun 2026 21:53:28 -0500 Subject: [PATCH] docs: update SilverSight AGENTS.md with GitHub repo reference SilverSight repo: https://github.com/allaunthefox/SilverSight All new formal work goes to the SilverSight repository. --- 0-Core-Formalism/lean/SilverSight/AGENTS.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/0-Core-Formalism/lean/SilverSight/AGENTS.md b/0-Core-Formalism/lean/SilverSight/AGENTS.md index cd4f8c68..177102db 100644 --- a/0-Core-Formalism/lean/SilverSight/AGENTS.md +++ b/0-Core-Formalism/lean/SilverSight/AGENTS.md @@ -2,7 +2,13 @@ **SilverSight is the clean-slate rebase of the Research Stack.** -## Location +## Repository + +**GitHub:** `https://github.com/allaunthefox/SilverSight` +**Local clone:** `/tmp/SilverSight` (or wherever you clone it) +**Formal modules:** `formal/SilverSight/` + +## Location (in Research Stack — for lake build integration) ``` 0-Core-Formalism/lean/SilverSight/ @@ -18,7 +24,7 @@ ## Rules -1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes here. +1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes to the SilverSight repository. 2. **Imports from Semantics are allowed** (cross-project): `import Semantics.FixedPoint`, `import Semantics.Spectrum`, etc.