Function expr_const_matches_by_address

crates/kernel/src/congruence.rs:522–530

()

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

    let lean_e = env::Expr::cnst(name.clone(), vec![]);
    let zero_e = KExpr::<Anon>::cnst(KId::new(addr, ()), Box::new([]));
    expr_congruent(&lean_e, &zero_e, &r).unwrap();
  }

  #[test]
  fn expr_const_addr_mismatch_fails() {