Test well_formed_adt
Source location: crates/formality-rust/src/prove/test/adt_wf.rs:30
#[test]
fn well_formed_adt() {
let assumptions: Wcs = Wcs::t();
let goal: Parameter = term("X<u32>");
let constraints = prove(
decls(),
Env::default(),
assumptions,
Predicate::WellFormed(goal),
);
constraints.assert_ok(
expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Rules proved (8)
Premises failed (0)
This test records no negative coverage.
Proof trees
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (parameter well formed)prove_wc.rs:154args
prove_wf (ADT)prove_wf.rs:65args
for_allcombinators.rs:69prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (parameter well formed)prove_wc.rs:154args
prove_wf (integers and booleans)prove_wf.rs:56args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args