Positive coverage: transitive_reachable / transitive
transitive| Line | Coverage | Source |
|---|---|---|
| 37 | ✗ | (transitive_reachable(graph, a) => b) |
| 38 | ✗ | (transitive_reachable(graph, b) => c) |
| ──────── ("transitive") | ||
| 40 | 2 | (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
transitive_reachable (base)test_filtered.rs:31transitive_reachable (transitive)test_filtered.rs:39transitive_reachable (base)test_filtered.rs:31transitive_reachable (base)test_filtered.rs:31
transitive_reachable (transitive)test_filtered.rs:39transitive_reachable (base)test_filtered.rs:31transitive_reachable (transitive)test_filtered.rs:39transitive_reachable (base)test_filtered.rs:31transitive_reachable (base)test_filtered.rs:31
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
transitive_reachable (transitive)test_reachable.rs:39transitive_reachable (base)test_reachable.rs:32transitive_reachable (transitive)test_reachable.rs:39transitive_reachable (base)test_reachable.rs:32transitive_reachable (base)test_reachable.rs:32
transitive_reachable (base)test_reachable.rs:32transitive_reachable (transitive)test_reachable.rs:39transitive_reachable (base)test_reachable.rs:32transitive_reachable (base)test_reachable.rs:32
transitive_reachable (transitive)test_reachable.rs:39transitive_reachable (base)test_reachable.rs:32transitive_reachable (transitive)test_reachable.rs:39transitive_reachable (base)test_reachable.rs:32transitive_reachable (base)test_reachable.rs:32