lthms @lthms@mastodon.social

My better half, genuinely : “Oh right, you’re old, you don’t know that.

I really am looking forward to see how Lean evolves in the future. It really looks like they want to build something more akin to Idris than Coq, i.e., a functional language backed by a theorem prover, and not the other way around.

where are the comments? what am I supposed to care about?

ocamlgraph may be a great library, but I feel the documentation is a bit… lacking.

Here what the `demo' module in the examples looks like: https://github.com/backtracking/ocamlgraph/blob/master/examples/demo.ml

> Showing 320 changed files with 42 additions and 147,948 deletions.

https://github.com/clarus/coq-of-ocaml/commit/7651504c124e53c5b0640ef095d99a71585e4724

😎

Hi @raichoo! I am currently experimenting with hikari, thanks for implementing it!

I’ve a question, though. Is there a way to scale a given output by a given factor? I couldn’t find it in the man pages :o

(borrowing the idea from @MartinShadok :D)

Who will win?

Friendly reminder that https://github.com/lthms/coq-MiniHTTPServer exists and I am pretty proud of it 💓

One exception though: I’ve build OCaml and Coq way too many times.

Random anecdote: I’ve started using “local switch” (`opam switch create .`) a few months ago, and it made my development workflows way more manageable than before.

For better or worst, it’s live: https://soap.coffee/~lthms/ 🎉

Still need to do some writing, though.

it’s not as ready as I’d hope, but I think I will push it as is for now. Just want to see it live.

Okay, so challenge of the week-end: finishing this website redesign. Fun thing is: what’s remaining is mostly describing the changes in the respective literate program documents 😅 @dmbaturin I will definitely ping you when I’m finished describing the side notes