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

Class BlockResult

crates/ffi/src/lean_env.rs:1908–1912  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

1906/// Available in the main `ix` binary (unlike the other `#[cfg(feature =
1907/// "test-ffi")]` helpers in this file) because `ix validate --path <file>`
1908/// uses it to run the full compile → decompile → roundtrip → nested-detect
1909/// pipeline on arbitrary Lean files. The `validate-aux` test suite in
1910/// `Tests/Ix/Compile/ValidateAux.lean` also calls this FFI via
1911/// `ix_rs_test`, but it's not gated on test-ffi any more — same function,
1912/// same binary entry point, just two callers.
1913///
1914/// Returns total failure count across all phases.
1915///

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected