feat: start Std package
This commit is contained in:
parent
83d1b62a99
commit
efba802011
2 changed files with 14 additions and 0 deletions
7
src/Std/Data.lean
Normal file
7
src/Std/Data.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue