Diamond Types insertion scan
Motivation for preserving exact origins and record identity; no formal Rust refinement.
A remote record's ordinal within a shared source gap is exact
Proof verified
complete
References are added by contributors. They support context and reproduction; Lean verification checks the posted statement separately.
Add a source
Sign in to contribute.