Function expr_let_matches

crates/kernel/src/congruence.rs:606–623

()

  #[test]
  fn expr_let_matches() {
    let r = empty_resolver();
    let lean_e = env::Expr::letE(
      mk_name("x"),
      env::Expr::sort(LL::zero()),
      env::Expr::bvar(n(0)),
      env::Expr::bvar(n(0)),
      false,
    );
    let zero_e = KExpr::<Anon>::let_(
      (),
      KExpr::sort(KUniv::zero()),
      KExpr::var(0, ()),
      KExpr::var(0, ()),
      false,
    );
    expr_congruent(&lean_e, &zero_e, &r).unwrap();
  }

  #[test]
  fn expr_mdata_is_transparent() {