From ce29de1b49aa7d6790c82ea68ca14d0a19168552 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 20 May 2018 13:26:59 -0700
Subject: [PATCH] chore(util): style

---
 src/util/name.cpp     | 4 ++--
 src/util/name.h       | 2 +-
 src/util/object_ref.h | 3 ++-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/util/name.cpp b/src/util/name.cpp
index 6ffd2cf14c..c1e22026ca 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -92,14 +92,14 @@ name::name(name const & prefix, char const * n):
                         prefix.raw(), mk_string(n), sizeof(unsigned))) {
     size_t sz  = strlen(n);
     unsigned h = hash_str(static_cast<unsigned>(sz), n, prefix.hash());
-    cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h);
+    cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h); // NOLINT
 }
 
 name::name(name const & prefix, unsigned k):
     object_ref(mk_cnstr(static_cast<unsigned>(name_kind::NUMERAL),
                         prefix.raw(), mk_nat_obj(k), sizeof(unsigned))) {
     unsigned h = ::lean::hash(k, prefix.hash());
-    cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h);
+    cnstr_set_scalar<unsigned>(raw(), 2*sizeof(object*), h); // NOLINT
 }
 
 name::name(std::initializer_list<char const *> const & l):name() {
diff --git a/src/util/name.h b/src/util/name.h
index 02bd0da254..585a235d0b 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -53,7 +53,7 @@ public:
     static char const * get_string(object * o) { return c_str(get_string_obj(o)); }
     static object * get_num_obj(object * o) { return cnstr_obj(o, 1); }
     static unsigned get_numeral(object * o) { return unbox(cnstr_obj(o, 1)); }
-    static unsigned hash(object * o) { return cnstr_scalar<unsigned>(o, 2*sizeof(object*)); }
+    static unsigned hash(object * o) { return cnstr_scalar<unsigned>(o, 2*sizeof(object*)); } // NOLINT
     static bool eq_core(object * o1, object * o2);
     static int cmp(object * o1, object * o2);
     size_t size_core(bool unicode) const;
diff --git a/src/util/object_ref.h b/src/util/object_ref.h
index 43c6d322d4..782a3d5d85 100644
--- a/src/util/object_ref.h
+++ b/src/util/object_ref.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <algorithm>
 #include "runtime/object.h"
 
 namespace lean {
@@ -53,7 +54,7 @@ inline object_ref mk_cnstr(unsigned tag, object_ref const & r1, object_ref const
 }
 /* The following definition is a low level hack that relies on the fact that sizeof(object_ref) == sizeof(object *). */
 inline object_ref const & cnstr_obj_ref(object_ref const & ref, unsigned i) {
-    static_assert(sizeof(object_ref) == sizeof(object *), "unexpected object_ref size");
+    static_assert(sizeof(object_ref) == sizeof(object *), "unexpected object_ref size"); // NOLINT
     lean_assert(is_cnstr(ref));
     return reinterpret_cast<object_ref const *>(reinterpret_cast<char*>(ref.raw()) + sizeof(constructor))[i];
 }