mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
fa8f6a2586
Utility scripts: - download_leanstral.py: HuggingFace model download for autoproof - download_leanstral_urllib.py: stdlib-only variant - prime_slos_explore.py: spectral signature exploration for primes Infrastructure: - scripts/mcp_backend/: Rust MCP backend (src + Cargo.toml/lock, target/ gitignored) Data: - .openresearch/artifacts/slos_checkpoints/: 128K checkpoint data - archive/dead_code_2026-07-03/: 360K archived dead code
10 lines
229 B
Text
10 lines
229 B
Text
namespace Test
|
||
|
||
structure Chain (X : Type) where
|
||
pred : ℕ → X → Prop
|
||
nested (k : ℕ) (x : X) (h : pred k x) : pred (k.succ) x
|
||
|
||
def admissible (X : Type) (c : Chain X) (k : ℕ) (x : X) : Prop :=
|
||
c.pred k x
|
||
|
||
end Test
|