1  # examples/lean/BUCK
 2  #
 3  # Lean 4 examples using hermetic Nix toolchain
 4  
 5  load("@toolchains//:lean.bzl", "lean_binary")
 6  
 7  lean_binary(
 8      name = "hello",
 9      srcs = ["Hello.lean"],
10      visibility = ["PUBLIC"],
11  )
12  
13  lean_binary(
14      name = "hashmap",
15      srcs = ["HashMap.lean"],
16      visibility = ["PUBLIC"],
17  )