scratches/ffi_test
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
ffi_test/FfiTest/Basic.lean

7 lines
105 B
Text
Raw Permalink Normal View History

ffi example (from official lake repository (leanprover/lean4))
2024-10-25 16:47:35 +09:00
@[extern "my_add"]
opaque myAdd : UInt32 → UInt32 → UInt32
def hello := "world"
-- #eval myAdd 1 2
Reference in a new issue Copy permalink