Positive coverage: sum_all / sum
sum| Line | Coverage | Source |
|---|---|---|
| 62 | N/A | (let acc: Num = Num(0)) |
| 63 | ✗ | (for_all(n in nums) with(acc) (let acc: Num = Num(acc.0 + n.0))) |
| ──────── ("sum") | ||
| 66 | 2 | (sum_all(nums) => acc) |
2 tests exercised this rule:
Source location: crates/formality-core/src/judgment/test_for_all.rs:74
#[test]
fn test_for_all_with_accumulator() {
let nums = vec![Num(1), Num(2), Num(3)];
sum_all(nums).assert_ok(expect_test::expect!["{Num(6)}"]);
}Proof tree
sum_all (sum)test_for_all.rs:65
Source location: crates/formality-core/src/judgment/test_for_all.rs:80
#[test]
fn test_for_all_with_accumulator_empty() {
let nums: Vec<Num> = vec![];
sum_all(nums).assert_ok(expect_test::expect!["{Num(0)}"]);
}Proof tree
sum_all (sum)test_for_all.rs:65