From 049259b47f8ca87d6bd46cab040b0be5ac888236 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 9 Jun 2022 20:29:44 -0400 Subject: [PATCH] fix: delete duplicate improperly case `Ffi.lean` --- examples/ffi/lib/lean/Ffi.lean | 5 ----- 1 file changed, 5 deletions(-) delete mode 100644 examples/ffi/lib/lean/Ffi.lean diff --git a/examples/ffi/lib/lean/Ffi.lean b/examples/ffi/lib/lean/Ffi.lean deleted file mode 100644 index 9ba99565ca..0000000000 --- a/examples/ffi/lib/lean/Ffi.lean +++ /dev/null @@ -1,5 +0,0 @@ -@[extern "my_add"] -constant myAdd : UInt32 → UInt32 → UInt32 - -@[extern "my_lean_fun"] -constant myLeanFun : IO PUnit