premise `let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?`

Premise at line 588. Observed failure causes: inapplicable.

struct

Line	Coverage	Source
588	1	(let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?)
589	✗	(if turbofish.parameters.len() == binder.len())
590	✗	(let StructBoundData { where_clauses, fields } = binder.instantiate_with(&turbofish.parameters)?)
593	N/A	(let expected_names: Set<FieldName> = for_all field in fields => field.name)
594	N/A	(let provided_names: Set<FieldName> = for_all field in field_exprs => field.name)
595	✗	(if expected_names == provided_names)
599	1	(if field_exprs.len() == provided_names.len())
602	✗	(for_all(i in 0..field_exprs.len()) with(state) (field in fields) (if field.name == field_exprs[i].name) (borrow_check_expr_has_ty(env, assumptions, state, &field_exprs[i].value, &field.ty, places_live_on_exit) => state))
607	✗	(prove_where_clauses(env, assumptions, state, where_clauses) => state)
609	N/A	(let ty = RigidTy::new(adt_id, &turbofish.parameters))
		──────── ("struct")
611	19	(borrow_check_expr(env, assumptions, state, Expr::Struct { adt_id, turbofish, field_exprs }, places_live_on_exit) => (ty, state))

1 test failed proving this premise:

Source location: tests/mir_typeck.rs:876 (all coverage from this test)

fn foo (v1: u32) -> u32 {
    let v2: u32 = Nonexistent { value: false };
    return v1;
}

Failed proof tree

Keyboard shortcuts