max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(runtime/int64): compilation issue on Linux

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-24 07:58:22 -07:00
parent b6decd70f0
commit 84de479a4c
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/runtime/int64.h
View file

@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <stdint.h>
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");
}