MCPcopy Create free account
hub / github.com/argumentcomputer/ix / AuxCompareEntry

Class AuxCompareEntry

crates/ffi/src/lean_env.rs:325–328  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

323
324/// Aux-`_N` rename map for alpha-collapsed nested auxiliaries.
325///
326/// When `perm` maps several source aux positions to one canonical slot,
327/// aux_gen names its regenerated patches after the MIN source position
328/// (`docs/ix_canonicity.md` §6.4); the other source `_N` names are address
329/// aliases (in-SCC collapse) or surgered originals (evaporated auxes of a
330/// split block). Either way, structural comparison of a regenerated patch
331/// against a source-order original must rename the non-representative

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected