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

Function infer_key_closed_expr_ignores_ctx

crates/kernel/src/tc.rs:1385–1392  ·  view source on GitHub ↗
()

Source from the content-addressed store, hash-verified

1383
1384 #[test]
1385 fn whnf_key_uses_suffix_across_different_outer_ctx() {
1386 // The suffix-aware key should let an open subterm hit cache across
1387 // different OUTER contexts when only the inner suffix matters.
1388 //
1389 // Both checkers push the same innermost local frame after a different
1390 // outer frame. A `var(0)` with lbr=1 should key only by the inner
1391 // suffix, so the two `whnf_key`s should match even though the outer
1392 // contexts (and hence ctx_ids) differ.
1393 let env: *mut KEnv<Meta> = Box::leak(Box::new(KEnv::<Meta>::new()));
1394 let e = var(0); // lbr = 1, depends only on innermost frame
1395 let (h1, ctx1, outer1) = {

Callers

nothing calls this directly

Calls 4

new_tcFunction · 0.85
push_localMethod · 0.80
infer_keyMethod · 0.80
sort0Function · 0.70

Tested by

no test coverage detected