Test well_formed_adt
Source location: crates/formality-rust/src/prove/test/adt_wf.rs:30
#[test]
fn well_formed_adt() {
let assumptions: Predicates = Predicates::t();
let goal: Parameter = term("X<u32>");
let constraints = prove(
decls(),
Env::default(),
assumptions,
AtomicPredicate::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_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (parameter well formed)prove_predicate.rs:150args
prove_wf (ADT)prove_wf.rs:65args
for_allcombinators.rs:69prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (parameter well formed)prove_predicate.rs:150args
prove_wf (integers and booleans)prove_wf.rs:56args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args