diff --git a/src/Std/Data.lean b/src/Std/Data.lean new file mode 100644 index 0000000000..c8a99e4082 --- /dev/null +++ b/src/Std/Data.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +-- import Std.Data.BinomialHeap +def test := 10 diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 9a861bc9c0..64fc61b574 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -17,4 +17,11 @@ stdlib: "OLEAN_OUT=${LIB}/lean"\ "LEANC_OPTS=${LEANC_OPTS}"\ "MORE_DEPS=${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}";\ + "${LEAN_BIN}/leanmake" lib\ + PKG=Std\ + "OUT=${LIB}"\ + "LIB_OUT=${LIB}/lean"\ + "OLEAN_OUT=${LIB}/lean"\ + "LEANC_OPTS=${LEANC_OPTS}"\ + "MORE_DEPS=${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}";\ fi