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

Premise at line 511. Observed failure causes: inapplicable.

struct

Line	Coverage	Source
511	1	(let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?)
512	✗	(if turbofish.parameters.len() == binder.len())
513	✗	(let StructBoundData { where_clauses, fields } = binder.instantiate_with(&turbofish.parameters)?)
516	N/A	(let expected_names: Set<&FieldName> = fields.iter().map(\|f\| &f.name).collect())
517	N/A	(let provided_names: Set<&FieldName> = field_exprs.iter().map(\|fe\| &fe.name).collect())
518	✗	(if expected_names == provided_names)
521	✗	(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))
526	✗	(prove_where_clauses(env, assumptions, state, where_clauses) => state)
528	N/A	(let ty = RigidTy::new(adt_id, &turbofish.parameters))
		──────── ("struct")
530	7	(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