Test `vec_vec_u32_debug`

Source location: crates/formality-rust/src/prove/test/simple_impl.rs:30

#[test]
fn vec_vec_u32_debug() {
    let goal: Predicate = term("Debug(Vec<Vec<u32>>)");
    prove(decls(), (), (), goal).assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}

Rules proved (9)

Judgment	Rule	All tests of this rule
prove_after	prove_after	237 tests
prove_eq	existential	223 tests
prove_eq	rigid	201 tests
prove_eq	symmetric	220 tests
prove_existential_var_eq	existential-nonvar	56 tests
prove_predicate	eq	231 tests
prove_predicate	positive impl	219 tests
prove_predicate_list	none	238 tests
prove_predicate_list	some	237 tests

Premises failed (0)

This test records no negative coverage.

Proof trees

Proof tree

prove_predicate_list (some) prove_predicate_list.rs:28
- args
- prove_predicate (positive impl) prove_predicate.rs:79
  - args
  - scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_eq (rigid) prove_eq.rs:48
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_eq (symmetric) prove_eq.rs:39
    
    args
    
    prove_eq (existential) prove_eq.rs:63
    
    args
    
    prove_existential_var_eq (existential-nonvar) prove_eq.rs:96
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_eq (rigid) prove_eq.rs:48
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_eq (symmetric) prove_eq.rs:39
    
    args
    
    prove_eq (existential) prove_eq.rs:63
    
    args
    
    prove_existential_var_eq (existential-nonvar) prove_eq.rs:96
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
- prove_after (prove_after) prove_after.rs:20
  - args
  - prove_predicate_list (none) prove_predicate_list.rs:21
    
    args

How to read this page

Keyboard shortcuts

A MIR Formality

Test vec_vec_u32_debug

Rules proved (9)

Premises failed (0)

Proof trees

Test `vec_vec_u32_debug`