Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: transitive_reachable / transitive

transitive
LineCoverageSource
37(transitive_reachable(graph, a) => b)
38(transitive_reachable(graph, b) => c)
──────── ("transitive")
402(transitive_reachable(graph, a) => c)

2 tests exercised this rule:


Source location: crates/formality-core/src/judgment/test_filtered.rs:55

#[test]
fn judgment() {
    let graph = Arc::new(Graph {
        edges: vec![(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)],
    });

    transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#"
        the rule "base" at (test_filtered.rs) failed because
          condition evaluated to false: `b % 2 == 0`"#]]);

    transitive_reachable(&graph, 2).assert_ok(expect_test::expect!["{4, 8, 10}"]);
}
Proof tree

Source location: crates/formality-core/src/judgment/test_reachable.rs:51

#[test]
fn judgment() {
    let graph = Arc::new(Graph {
        edges: vec![(0, 1), (1, 2), (2, 0), (2, 3)],
    });

    transitive_reachable(graph, 0).assert_ok(expect_test::expect!["{0, 1, 2, 3}"]);
}
Proof tree