lean4-htt/tests/compiler/link_lake.lean
2023-07-21 09:19:19 +02:00

5 lines
127 B
Text

-- this should be sufficient to trigger linking against Lake's initializer symbols
import Lake
def main : IO Unit :=
return