diff --git a/README.md b/README.md
index 476bb27..6d007dd 100644
--- a/README.md
+++ b/README.md
@@ -8,3 +8,36 @@ This is based on:
 * [Rustonomicon FFI](https://doc.rust-lang.org/nomicon/ffi.html)
 * [Rust Bindgen](https://rust-lang.github.io/rust-bindgen/introduction.html)
 * [Rust Bindgen Static Functions](https://github.com/rust-lang/rust-bindgen/discussions/2405)
+
+## Usage
+
+Since the entire environment was built on Nix flakes, the easiest way to run the executable is via Nix:
+```
+$ nix run .#caller
+```
+For interactive development, one can also drop into a develop shell:
+```
+$ nix develop
+```
+and then execute
+```
+$ cargo run
+```
+Execution without Nix is possible.
+
+This project has been tested on Linux and Mac OS.
+
+## Structure
+
+The project has 2 parts:
+1. `Callee`, a Lean library
+2. `Caller`, a Rust executable
+
+`Caller` is dependent on `Callee` and requires it along with Lean to be present
+in the environment for linking. Specifically the following environment variables
+must be set:
+* `CALLEE_PATH`: Path to a directory containing `libCallee.so`
+* `LEAN_ROOT`: Path to a directory such that `$LEAN_ROOT/include` has lean
+  headers and `$LEAN_ROOT/lib` has the `leanshared` library
+* Clang path must be set so `clang-sys` can find it
+* Clang executable must be present in `PATH`
diff --git a/src/main.rs b/src/main.rs
index e8ec002..5beb1d1 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -11,8 +11,14 @@ mod lean {
 		pub fn lean_initialize();
 		// lean_io_mark_end_initialization is already defined.
 	}
+}
+
+mod callee {
+	use super::lean::*;
+
 	#[link(name = "Callee")]
 	extern "C" {
+		#[allow(non_snake_case)]
 		pub fn initialize_Callee(builtin: u8, world: *mut lean_object) -> *mut lean_object;
 		pub fn my_function(s: lean_obj_arg) -> lean_obj_arg;
 	}
@@ -22,7 +28,7 @@ fn main() {
 		lean::lean_initialize_runtime_module();
 		lean::lean_initialize();
 		let builtin: u8 = 1;
-		let res = lean::initialize_Callee(builtin, lean::lean_io_mk_world());
+		let res = callee::initialize_Callee(builtin, lean::lean_io_mk_world());
 		if lean::lean_io_result_is_ok(res) {
 			lean::lean_dec_ref(res);
 		} else {
@@ -37,7 +43,7 @@ fn main() {
 	let c_str = std::ffi::CString::new("hello ").unwrap();
 	let result = unsafe {
 		let native_str = lean::lean_mk_string(c_str.as_ptr());
-		let result_obj = lean::my_function(native_str);
+		let result_obj = callee::my_function(native_str);
 		let result_c_str = std::ffi::CStr::from_ptr(lean::lean_string_cstr(result_obj));
 		let str = result_c_str.to_str().unwrap().to_string();
 		// Clean up the resultant objects