Function expr_proj_field_mismatch_fails

crates/kernel/src/congruence.rs:664–673

()

  #[test]
  fn expr_proj_field_mismatch_fails() {
    let name = mk_name("MyStruct");
    let addr = mk_addr("MyStruct");
    let r = resolver_with(&[(name.clone(), addr.clone())]);

    let lean_e = env::Expr::proj(name.clone(), n(2), env::Expr::bvar(n(0)));
    let zero_e = KExpr::<Anon>::prj(KId::new(addr, ()), 1, KExpr::var(0, ()));
    let e = expr_congruent(&lean_e, &zero_e, &r).unwrap_err();
    assert!(e.contains("proj field mismatch"));
  }

  #[test]
  fn expr_fvar_unexpected() {