diff --git a/examples/file.ivory b/examples/file.ivory
new file mode 100644
--- /dev/null
+++ b/examples/file.ivory
@@ -0,0 +1,391 @@
+-- # -*- mode: haskell -*-
+
+import (stdio.h, printf) int32_t printf(string x)
+import (stdio.h, printf) int32_t printf2(string x, int32_t y)
+
+include concreteIvory --for printf definitions in ConcreteFile.hs
+include stdlibStringModule
+
+-- extern foo.h G* uint8_t myptr
+
+-- A top level definition.
+bar = 3 + 2;
+
+-- Define a top-level type alias.
+type Boo = int8_t;
+
+-- (Both of the above can be done on Haskell and you can use antiquotation.)
+
+-- Define a struct. A base type is turned into a memory area by adding a
+-- '&'. Note this is a type-level operator. Arrays and structs are always memory
+-- areas.
+struct Bar00 {
+  &int32_t aBar00;
+}
+
+struct Foo
+ { -- When context makes apparent and we can syntactically check the type, a
+   -- base type is promoted to a memory area (i.e., bool is rewritten to &bool).
+   bool aFoo
+   -- '&' at the type level binds most tightly and is right-associative. When
+   -- we use a type alias, the '&' must be added explicitly.
+ ; &SomeInt[4] aBar
+ }
+
+-- Safe string structs: strings of max length 16 bytes Generates two field
+-- labels: stringLengthL (int32_t) and stringDataL (array uint8_t[4]). The type
+-- of the struct is ivory_string_FooStr. See the String library in ivory-stdlib
+-- for some string library functions.
+string struct FooStr 4
+
+-- Nested struct references
+struct Foo2
+  { struct Foo foo2f
+  }
+
+r* struct ivory_string_FooStr foostr(r* struct ivory_string_FooStr s) {
+  -- Allocate a new string dynamic string. Fails if the string is too large.
+  alloc s0{} = $stringInit("foo");
+  foostr(s0);
+  -- Store a new string into the dynamic string data structure.
+  $string_lit_store("foos", s);
+  return s;
+}
+
+-- Declaring abstract structs
+-- abstract struct fooStruct "foobar/foo.h"
+
+-- Struct declared with C-like types
+struct Goo
+ { int32_t aGoo;
+   bool bGoo;
+   int32_t[4] cGoo;
+ }
+
+-- Use the expression and alias
+Boo foo(Boo x) {
+  return (bar + x);
+}
+
+-- Calling builtin functions
+void foo67(* float a)
+{ store a as sin(*a);
+}
+
+-- if-the-else blocks.  Braces are mandatory.
+int32_t foo1() {
+  if (true) {
+    let a = 5;
+    return a;
+  }
+  else {
+    let b = 3;
+    return b + 3;
+  }
+}
+
+-- Empty statements in if-then-else
+void foo30(Boo x) {
+  if(true) {}
+  else { return; }
+  return;
+}
+
+-- Using an external symbol. Don't run this, unless the header is in-scope.
+-- uint8_t foo31() {
+--   return (3 + *myptr);
+-- }
+
+-- Allocation on the stack (dereference is an expression)
+int32_t foo0() {
+  alloc *x = 3;
+  store x as 4;
+  return *x + 4;
+}
+
+
+-- Global allocation (G), stack allocation (S), and undetermined scope (var c)
+uint8_t foo12(* uint8_t a, G*uint8_t b, * uint8_t c, S* uint8_t d) {
+  store b as *a;
+  return *b + *c + *d;
+}
+
+-- Allocated on either the stack or globally, with user-provided type-variable (xx).
+xx* uint32_t foo14(xx* struct Foo f) {
+  let a = f . aBar;
+  let u = a @ 2;
+  return u;
+}
+
+-- Allocate an array and index into it. A precondition is given for the function
+-- argument.
+uint32_t foo6(v *uint32_t[3] arr0) {
+  alloc arr1[] = {1,2,3};
+  map ix {
+    store arr0 @ ix as *arr1 @ ix;
+  }
+  -- Same as *arr0 @ 1 ;
+  return arr0[1] ;
+}
+{ pre(arr0[1] > 0);
+}
+
+-- Use a struct. Polymorphic region reference.
+void foo00(* int32_t[5] arr, * struct Bar00 str) {
+  -- The following two are equivalent
+  store arr @ 2 as 3;
+  store arr @ 2 as 4;
+  -- As well as the next two
+  store str.aBar00 as 1;
+  store str.aBar00 as 2;
+
+  store arr@2      as arr[3];
+}
+
+-- Boolean operators
+uint32_t foo7(bool b, uint32_t a) {
+    return (b && !b ? a+3 : signum(abs(a)) - 4);
+}
+
+void foo2() {return;}
+
+-- Function calls, with a return value and without.
+uint32_t foo8(bool b, uint32_t a) {
+    foo2();
+    let x = foo7(b, a);
+    foo7 (b, a);
+    return (b && !b ? a+3 : signum(abs(a)) - x);
+}
+
+-- Local assignment (constant).
+uint32_t foo9(uint32_t a) {
+  forever {
+    let b = a + 3;
+    return b;
+  }
+  return 0;
+}
+
+-- Memcopy.
+void foo10(*uint32_t[3] r0, *uint32_t[3] r1) {
+  memcpy r0 r1;
+}
+
+-- Const decorators.
+uint32_t foo11(const *uint32_t i) {
+  return *i;
+}
+
+-- Pre and post conditions.
+uint32_t foo15(uint32_t a, * struct Foo f, * struct Foo g) {
+        return a;
+}
+{ pre(a < 4);
+  pre(a > 0);
+  post(return > 5);
+  pre(* f . aFoo && * g . aFoo);
+}
+
+-- Stack allocated variable.
+uint32_t foo16(S*uint32_t i) {
+  return *i;
+}
+{ pre(*i > 3); }
+
+-- Global allocated variable.
+uint32_t foo17(G*uint32_t i) {
+  return *i;
+}
+
+-- allocate and initialize a struct.
+void foo92() {
+  alloc s{} = {aFoo = true};
+  return;
+}
+
+-- Mapping over an array
+void mapProc(*uint8_t[4] arr, uint8_t x) {
+  map ix {
+    let v = arr @ ix;
+    store v as *v + x;
+  }
+}
+
+-- Casting
+void foo57(* uint8_t a, * uint16_t b, * int8_t c, * int32_t d)
+{
+  store b as safeCast(*a);     -- can always safely cast
+  store b as castWith(3, *d);  -- cast with a default value if out of range
+  store c as twosCompCast(*a); -- interpret under 2s compliment
+}
+
+-- Statements and expression macros
+int32_t foo68(int32_t x, int32_t y) {
+  -- macroStmts is a Haskell function
+  $macroStmts(x, y);
+  -- with a return value (Ivory eff a)
+  a <- $macroStmtsRet(x, y);
+  -- macroExp is a Haskell function, too
+  if($macroExp(x, y)) { return x; }
+  else { return a; }
+}
+
+int32_t foo100(int32_t x) {
+  return x;
+}
+
+-- Calling functions (with return values) as expressions
+int32_t bar82() {
+  let y = foo100(4);
+  return foo100(foo100(y));
+}
+
+-- Fizzbuzz four ways
+void fizzbuzzUp() {
+  upTo 100 ix {
+    -- for typechecking
+    let (ix_t 101) ix' = ix;
+    let i = fromIx(ix);
+    if (i % 15 == 0) {
+      printf("Fizzbuzz");
+    } else {
+      if (i % 5 == 0) {
+        printf("Fizz");
+      } else {
+        if (i % 3 == 0) {
+          printf("Buzz");
+        } else { printf2("%i\n",i); }
+      }
+    }
+  }
+}
+
+void fizzbuzzUpFrom() {
+  upFromTo 50 100 ix {
+    -- for typechecking
+    let (ix_t 101) ix' = ix;
+    let i = fromIx(ix);
+    if (i % 15 == 0) {
+      printf("Fizzbuzz");
+    } else {
+      if (i % 5 == 0) {
+        printf("Fizz");
+      } else {
+        if (i % 3 == 0) {
+          printf("Buzz");
+        } else { printf2("%i\n",i); }
+      }
+    }
+  }
+}
+
+void fizzbuzzDown() {
+  downFrom 100 ix {
+    -- for typechecking
+    let (ix_t 101) ix' = ix;
+    let i = fromIx(ix);
+    if (i % 15 == 0) {
+      printf("Fizzbuzz");
+    } else {
+      if (i % 5 == 0) {
+        printf("Fizz");
+      } else {
+        if (i % 3 == 0) {
+          printf("Buzz");
+        } else { printf2("%i\n",i); }
+      }
+    }
+  }
+}
+
+void fizzbuzzDownFromTo() {
+  downFromTo 100 50 ix {
+    -- for typechecking
+    let (ix_t 101) ix' = ix;
+    let i = fromIx(ix);
+    if (i % 15 == 0) {
+      printf("Fizzbuzz");
+    } else {
+      if (i % 5 == 0) {
+        printf("Fizz");
+      } else {
+        if (i % 3 == 0) {
+          printf("Buzz");
+        } else { printf2("%i\n",i); }
+      }
+    }
+  }
+}
+
+------------------------------------------------------------
+-- Larger example (hypothetical pack and unpack functions). In practice, use
+-- ivory-serialize.
+int32_t unpackSint32(uint8_t a, uint8_t b, uint8_t c, uint8_t d)
+{
+  alloc *x = 0;
+  store x as safeCast(a) | safeCast(b) << 0x8 | safeCast(c) << 0x10 | safeCast(d) << 0x18;
+  return twosCompCast(*x);
+}
+
+int32_t unpack(* uint8_t[10] msg, int32_t ixx)
+{
+ let ix = toIx(ixx);
+ let res = unpackSint32( * msg @ ix
+                       , * msg @ (ix+1)
+                       , * msg @ (ix+2)
+                       , * msg @ (ix+3)
+                       );
+ return res;
+}
+
+void pack(*uint8_t[10] msg, int32_t x, int32_t ixx)
+{
+  let ix = toIx(ixx);
+  let ux = twosCompRep(x);
+  store msg @ ix     as bitCast(ux);
+  store msg @ (ix+1) as bitCast(ux >> 0x08);
+  store msg @ (ix+2) as bitCast(ux >> 0x10);
+  store msg @ (ix+3) as bitCast(ux >> 0x18);
+}
+
+struct Foo7 { struct ivory_string_FooStr aFoo7; }
+
+struct Bar2 { int32_t aBar7; }
+
+struct Boo { struct Bar2 aBoo; }
+
+void foobar (* struct Foo7 s) {
+  store (s . aFoo7 . stringDataL@0) as 3;
+  return;
+}
+
+int32_t bar72(int32_t x, * struct Boo a, * int32_t y, * int32_t[10] arr) {
+  store (a . aBoo) . aBar7 as *y;
+  store (a . aBoo) . aBar7 as *y;
+  store arr@toIx(*y + *y)   as *y + *y;
+  return a.aBoo->aBar7;
+}
+
+float tanFuncD(float x) {
+  return atan2(3.0, 1);
+}
+
+float tanFuncF(float x) {
+  return atan2(3.0, 1);
+}
+
+string struct Astr 4
+
+-- copy from an uint8_t array to a string
+void arr_to_str( * struct ivory_string_Astr s
+               , const * uint8_t[5] arr
+               ) {
+  $istr_from_sz(s, arr);
+}
+
+-- copy to an uint8_t array from a string
+void str_to_arr(* uint8_t[5] arr
+               , const * struct ivory_string_Astr s
+               ) {
+  $sz_from_istr(arr, s);
+}
diff --git a/ivory-examples.cabal b/ivory-examples.cabal
--- a/ivory-examples.cabal
+++ b/ivory-examples.cabal
@@ -1,5 +1,5 @@
 name:                ivory-examples
-version:             0.1.0.3
+version:             0.1.0.3.1
 author:              Galois, Inc
 maintainer:          trevor@galois.com, leepike@galois.com
 copyright:           2013 Galois, Inc.
@@ -11,6 +11,7 @@
 cabal-version:       >= 1.10
 license:             BSD3
 license-file:        LICENSE
+data-files:          examples/file.ivory
 source-repository    this
   type:     git
   location: https://github.com/GaloisInc/ivory