David Sheets

[RFC 3927](https://tools.ietf.org/html/rfc3927) states ``` The IPv4 prefix 169.254/16 is registered with the IANA for this purpose. The first 256 and last 256 addresses in the 169.254/16 prefix are reserved for...

http://tools.ietf.org/html/rfc6144 may be related. There is another ipv4 embedding block. We should check the semantic differences between all these v4-in-v6 embeddings.

#36 implements `cstruct` support. Changing this issue to track bigstring support only.

Also `create`.

I believe this issue is a general ctypes problem as you indicate. Once you clear it, you will surely find further issues with ctypes-on-osx. In particular, I believe a new...

While the tests still fail on OS X, the ctypes problem has been temporarily addressed in HEAD using the pkg-config solution described in ocamllabs/ocaml-ctypes#74.

I believe that a modified `↝*-irr-cont : ∀ { x y : Statement } { k' E E' e } → 𝒮 x [] E ~[ e ]↝* 𝒮 y...

https://github.com/jmlowenthal/agda-c/blob/348c56754376fd3a901f75ebb93d39402fae3cb3/src/C/Semantics/SmallStep/Properties/Program/Equivalence.agda#L46 becomes trivial to prove with this new `↝*-irr-cont`. It would seem that `↝-irr-cont` and `↝*-irr-cont` are then independent as the former asserts that any single reduction preserving its continuation...

I'm looking at the postulates in https://github.com/jmlowenthal/agda-c/blob/master/src/C/Semantics/SmallStep/Properties/Program/Equivalence.agda and hitting some issues with the representation of language constructs and semantic reductions. What is the reason that these types are records rather...

[From](http://lists.ocaml.org/pipermail/ctypes/2014-October/000109.html) the ctypes [mailing list](http://lists.ocaml.org/listinfo/ctypes): Adding support would mostly likely only involve changing ctypes itself, not OCaml-Java, and is likely to involve writing OCaml-Java implementations of the following components: (1)...