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

Premise at line 551. Observed failure causes: inapplicable.

struct

Line	Coverage	Source
551	1	(let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?)
552	✗	(if turbofish.parameters.len() == binder.len())
553	✗	(let StructBoundData { where_clauses, fields } = binder.instantiate_with(&turbofish.parameters)?)
556	N/A	(let expected_names: Set<&FieldName> = fields.iter().map(\|f\| &f.name).collect())
557	N/A	(let provided_names: Set<&FieldName> = field_exprs.iter().map(\|fe\| &fe.name).collect())
558	✗	(if expected_names == provided_names)
561	✗	(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))
566	✗	(prove_where_clauses(env, assumptions, state, where_clauses) => state)
568	N/A	(let ty = RigidTy::new(adt_id, &turbofish.parameters))
		──────── ("struct")
570	18	(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:648

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

Failed proof tree

Keyboard shortcuts