Function expr_proj_matches

crates/kernel/src/congruence.rs:653–661

()

  #[test]
  fn expr_proj_matches() {
    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(1), env::Expr::bvar(n(0)));
    let zero_e = KExpr::<Anon>::prj(KId::new(addr, ()), 1, KExpr::var(0, ()));
    expr_congruent(&lean_e, &zero_e, &r).unwrap();
  }

  #[test]
  fn expr_proj_field_mismatch_fails() {