Function expr_fvar_unexpected

crates/kernel/src/congruence.rs:676–682

()

  #[test]
  fn expr_fvar_unexpected() {
    let r = empty_resolver();
    let lean_e = env::Expr::fvar(mk_name("x"));
    let zero_e = KExpr::<Anon>::var(0, ());
    let e = expr_congruent(&lean_e, &zero_e, &r).unwrap_err();
    assert!(e.contains("Fvar") || e.contains("unexpected"));
  }

  #[test]
  fn expr_shape_mismatch_fails() {