[WIP] examples/bytestring

[quinn-dougherty]

with a very liberal "just append stuff till the executable stops complaining" approach toward making an edits file, I've almost gotten an examples/bytestring together.

I used a git submodule add to get the bytestring source in here.

Current bottleneck: "GHC.Prim.Notations is not a module" https://github.com/quinn-dougherty/hs-to-coq/blob/a69ccb3c1f23db22ac0ce6a99b9317ddfc097280/examples/bytestring/lib/Data/ByteString/Internal.v#L20 -- It doesn't appear to me that hs-to-coq is generating Notation modules in base, so I'm not sure what's going on. I get this error both when I stack exec hs-to-coq -- (in the standard common.mk) and when I run nixified result/bin/hs-to-coq.

the hs-to-coq execution seems to be going great! it's just outputting stuff that can't be coqc'd, or isn't successfully coqc'd according to the Makefile (which I wrote based on examples/containers/Makefile).

I super appreciate it if anyone has time to show me what I'm doing wrong. Also, totally open minded if you think it's not worth having this in examples dir.

[quinn-dougherty]

i'll back this out don't worry, was just testing something.