Function expr_bvar_matches

crates/kernel/src/congruence.rs:497–502

()

  #[test]
  fn expr_bvar_matches() {
    let r = empty_resolver();
    let lean_e = env::Expr::bvar(n(3));
    let zero_e = KExpr::<Anon>::var(3, ());
    expr_congruent(&lean_e, &zero_e, &r).unwrap();
  }

  #[test]
  fn expr_bvar_idx_mismatch_fails() {