From 84de479a4cfaa4bd7776eb3d40b203e1ec44a16e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Aug 2019 07:58:22 -0700 Subject: [PATCH] fix(runtime/int64): compilation issue on Linux --- src/runtime/int64.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/runtime/int64.h b/src/runtime/int64.h index 0e0ab738a3..243040d744 100644 --- a/src/runtime/int64.h +++ b/src/runtime/int64.h @@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include namespace lean { -typedef long long int64; -typedef unsigned long long uint64; -static_assert(sizeof(int64 ) == 8, "unexpected int64 size"); -static_assert(sizeof(uint64 ) == 8, "unexpected uint64 size"); +typedef int64_t int64; +typedef uint64_t uint64; +static_assert(sizeof(int64) == 8, "unexpected int64 size"); +static_assert(sizeof(uint64) == 8, "unexpected uint64 size"); }