enserpentiated

Author: kmill

src/Lean/Expr.lean

@@ -878,7 +878,7 @@ def isHave : Expr → Bool
   | letE (nonDep := nonDep) .. => nonDep
   | _       => false
 
-@[export lean_expr_isHave] def isHaveEx : Expr → Bool := isHave
+@[export lean_expr_is_have] def isHaveEx : Expr → Bool := isHave
 
 /-- Return `true` if the given expression is a metadata. -/
 def isMData : Expr → Bool

src/kernel/expr.cpp

@@ -295,10 +295,10 @@ bool is_default_var_name(name const & n) {
     return n == *g_default_name;
 }
 
-extern "C" uint8 lean_expr_isHave(object * e);
-bool let_nonDep_core(expr const & e) {
+extern "C" uint8 lean_expr_is_have(object * e);
+bool let_nondep_core(expr const & e) {
     lean_assert(is_let(e));
-    return lean_expr_isHave(e.to_obj_arg());
+    return lean_expr_is_have(e.to_obj_arg());
 }
 
 // =======================================
@@ -355,7 +355,7 @@ expr update_const(expr const & e, levels const & new_levels) {
 
 expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body) {
     if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_value) || !is_eqp(let_body(e), new_body))
-        return mk_let(let_name(e), new_type, new_value, new_body, let_nonDep(e));
+        return mk_let(let_name(e), new_type, new_value, new_body, let_nondep(e));
     else
         return e;
 }

src/kernel/expr.h

@@ -259,11 +259,11 @@ inline name const &    let_name(expr const & e)              { lean_assert(is_le
 inline expr const &    let_type(expr const & e)              { lean_assert(is_let(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
 inline expr const &    let_value(expr const & e)             { lean_assert(is_let(e)); return static_cast<expr const &>(cnstr_get_ref(e, 2)); }
 inline expr const &    let_body(expr const & e)              { lean_assert(is_let(e)); return static_cast<expr const &>(cnstr_get_ref(e, 3)); }
-bool                   let_nonDep_core(expr const & e);
-inline bool            let_nonDep(expr const & e) {
+bool                   let_nondep_core(expr const & e);
+inline bool            let_nondep(expr const & e) {
     lean_assert(is_let(e));
     bool r = lean_ctor_get_uint8(e.raw(), 4*sizeof(object*) + sizeof(uint64_t));
-    lean_assert(r == let_nonDep_core(e)); // ensure the C++ implementation matches the Lean one.
+    lean_assert(r == let_nondep_core(e)); // ensure the C++ implementation matches the Lean one.
     return r;
 }
 inline bool            is_shared(expr const & e)             { return !is_exclusive(e.raw()); }

src/kernel/expr_eq_fn.cpp

@@ -122,7 +122,7 @@ class expr_eq_fn {
                 apply(let_type(a), let_type(b), depth) &&
                 apply(let_value(a), let_value(b), depth) &&
                 apply(let_body(a), let_body(b), depth) &&
-                let_nonDep(a) == let_nonDep(b) &&
+                let_nondep(a) == let_nondep(b) &&
                 (!CompareBinderInfo || let_name(a) == let_name(b));
         }
         lean_unreachable(); // LCOV_EXCL_LINE

src/library/expr_lt.cpp

@@ -49,8 +49,8 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_ctx const * lctx
         else
             return is_lt(binding_body(a), binding_body(b), use_hash, lctx);
     case expr_kind::Let:
-        if (let_nonDep(a) != let_nonDep(b))
-            return let_nonDep(a) < let_nonDep(b);
+        if (let_nondep(a) != let_nondep(b))
+            return let_nondep(a) < let_nondep(b);
         else if (let_type(a) != let_type(b))
             return is_lt(let_type(a), let_type(b), use_hash, lctx);
         else if (let_value(a) != let_value(b))
@@ -159,8 +159,8 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
         else
             return is_lt_no_level_params(binding_body(a), binding_body(b));
     case expr_kind::Let:
-        if (let_nonDep(a) != let_nonDep(b))
-            return let_nonDep(a) < let_nonDep(b);
+        if (let_nondep(a) != let_nondep(b))
+            return let_nondep(a) < let_nondep(b);
         else if (is_lt_no_level_params(let_type(a), let_type(b)))
             return true;
         else if (is_lt_no_level_params(let_type(b), let_type(a)))

src/library/print.cpp

@@ -191,7 +191,7 @@ struct print_expr_fn {
     }
 
     void print_let(expr const & e) {
-        out() << (let_nonDep(e) ? "have " : "let ");
+        out() << (let_nondep(e) ? "have " : "let ");
         auto p = let_body_fresh(e);
         out() << p.second << " : ";
         print(let_type(e));