ffi.lean

import system.IO
import system.ffi
-- import config

-- This is all just config
set_option native.library_path "/Users/jroesch/Git/lean/build/debug"
set_option native.include_path "/Users/jroesch/Git/lean/src"
-- This flag controls whether lean will automatically invoke C++
-- set_option native.compile false
set_option native.emit_dwarf true
-- set_option trace.compiler true

open ffi
open ffi.type
open ffi.base_type

constant put_int : extern void "put_int" [int]
attribute [extern] put_int

definition main : IO unit := do
  i <- new (base int),
  write_nat_as_int 1337 i,
  put_int i