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

Class Level

crates/common/src/env.rs:276–276  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

274/// (`_private.….«0».…`, `Lean.Order.«term_⊑_»`) while [`Name::pretty`]
275/// renders them bare, so a fail-out file written by one side misses a
276/// string-keyed lookup on the other. Stripping the guillemets from BOTH
277/// the request and the candidate collapses the two renderings onto one
278/// key, at the cost of the same flattening ambiguity `pretty` already
279/// has. Mirrors `Ix.Cli.ConstsFile.normalizeName` on the Lean side.

Callers 7

zeroMethod · 0.70
succMethod · 0.70
maxMethod · 0.70
imaxMethod · 0.70
paramMethod · 0.70
mvarMethod · 0.70
ground_levelFunction · 0.50

Calls

no outgoing calls

Tested by

no test coverage detected