()
| 531 | |
| 532 | #[test] |
| 533 | fn expr_const_addr_mismatch_fails() { |
| 534 | let name = mk_name("Nat"); |
| 535 | let r = resolver_with(&[(name.clone(), mk_addr("Nat"))]); |
| 536 | |
| 537 | let lean_e = env::Expr::cnst(name.clone(), vec![]); |
| 538 | // Wrong address in zero_e |
| 539 | let zero_e = |
| 540 | KExpr::<Anon>::cnst(KId::new(mk_addr("Bogus"), ()), Box::new([])); |
| 541 | let e = expr_congruent(&lean_e, &zero_e, &r).unwrap_err(); |
| 542 | assert!(e.contains("address mismatch")); |
| 543 | } |
| 544 | |
| 545 | #[test] |
| 546 | fn expr_const_name_missing_from_resolver_fails() { |
nothing calls this directly
no test coverage detected