()
| 624 | |
| 625 | #[test] |
| 626 | fn expr_mdata_is_transparent() { |
| 627 | let r = empty_resolver(); |
| 628 | // Lean Mdata(_, Sort 0) must match the bare zero Sort 0. |
| 629 | let inner = env::Expr::sort(LL::zero()); |
| 630 | let lean_e = env::Expr::mdata(vec![], inner); |
| 631 | let zero_e = KExpr::<Anon>::sort(KUniv::zero()); |
| 632 | expr_congruent(&lean_e, &zero_e, &r).unwrap(); |
| 633 | } |
| 634 | |
| 635 | #[test] |
| 636 | fn expr_nat_lit_matches() { |
nothing calls this directly
no test coverage detected