Layer 0 substrate round 4: Reflect.lean — bidirectional CTerm/CType ↔ Lean.Expr

Browse source

Per THEORY.md §0.9 — reflection metaprogramming layer.  Bidirectional
bridge between the engine's first-class CTerm / CType inductives and
Lean's tactic-facing Lean.Expr representation.  Required for tactics
to inspect cubical terms and consult the contract registry.

· reflectULevel / reflectCType / reflectCTerm: per-constructor
  Expr-construction with explicit ULevel arguments emitted at every
  implicit-position (Expr-level construction is fully explicit).
· reifyULevel / reifyCType / reifyCTerm: per-constructor Expr-pattern
  inverses; level-coherence proofs discharged via hA ▸ A coercion
  where the recovered level disagrees with the explicit-position level.
· Contract registry: IO.Ref (Std.HashMap Lean.Name ContractEntry)
  with register / lookupByName / allRegistered.  Local `abbrev
  Contract` re-export to avoid the Reflect ↔ Contract circular
  dependency.
· 4 sorry'd round-trip theorems with substantive Prop statements
  awaiting the meta-level Expr-elaboration framework.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

...

This commit is contained in:

Maximus Gorog 2026-05-05 14:50:51 -06:00

parent 7ca4ac8d6a

commit 2f343b0980

1 changed files with 1410 additions and 0 deletions

Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL

Show stats Download patch file Download diff file Expand all files Collapse all files

1410

CubicalTransport/Reflect.lean Normal file

View file

File diff suppressed because it is too large Load diff