()
| 512 | |
| 513 | #[test] |
| 514 | fn expr_sort_matches() { |
| 515 | let r = empty_resolver(); |
| 516 | let lean_e = env::Expr::sort(LL::zero()); |
| 517 | let zero_e = KExpr::<Anon>::sort(KUniv::zero()); |
| 518 | expr_congruent(&lean_e, &zero_e, &r).unwrap(); |
| 519 | } |
| 520 | |
| 521 | #[test] |
| 522 | fn expr_const_matches_by_address() { |
nothing calls this directly
no test coverage detected