Function expr_nat_lit_matches

crates/kernel/src/congruence.rs:636–642

()

  #[test]
  fn expr_nat_lit_matches() {
    let r = empty_resolver();
    let lean_e = env::Expr::lit(Literal::NatVal(n(42)));
    // Nat expr construction for the zero kernel.
    let zero_e = KExpr::<Anon>::nat(n(42), mk_addr("any"));
    expr_congruent(&lean_e, &zero_e, &r).unwrap();
  }

  #[test]
  fn expr_str_lit_matches() {