Some time ago, I saw a toot with a link to a #Coq proof involving real numbers, but I can't find it anymore :(

I think it was about proving that the ratio of two Fibonacci numbers converges to the golden ratio, but I'm not sure.

Anyone remembers it and knows where I can find it?

#SILE hacking: finally got around to writing a little grammar for writing math in a TeX-like style (left) rather than in MathML directly (right).

Which one do you prefer? 😜

So after a few days at working with #c2hs to make bindings to #sundials in #haskell, I'm actually impressed by it.

It's a tool to help with writing bindings to C library. It can generate a lot of the boilerplate associated with this sort of stuff (e.g., generating wrapper types on the Haskell side) and typechecks the FFI imports by analyzing the C types in the library's headers.

PhD student at the University of Nottingham ⋅ Interested in functional programming (Haskell, OCaml), modeling languages and synchronous languages

Joined Jan 2018