Zulip Chat Archive
Stream: lean4
Topic: Generic external C function import
Number Eighteen (May 10 2024 at 07:57):
Hello all;
due to the lack of many native IO functions in Lean(e.g. to get current time), for each project I have to write extern
declarations, create a C subfolder to get the functions I want from the standard library and write the FFI and compilation instructions (which I am not good at).
Is there a way to import a function from the C standard library without having to go through all this hassle each time? By "way" I mean for example a keyword like extern stdlib
to tell the compiler/linker that this is the function from the C standard library? Or at least something that sidesteps the need to create an entire subproject folder just for a function?
Henrik Böving (May 10 2024 at 08:10):
You can use https://github.com/tydeu/lean4-alloy
Last updated: May 02 2025 at 03:31 UTC