Show newer

I just realized I have a Windows machine, that I could use to test the portability of stuff. I didn't realize earlier because I spend so much time in a Linux VM...

coqdoc is packaged as part of Coq, so projects stuck on older versions don't benefit from bugfixes and new features. That's sad. I've been wanting to split it off[1] but actually the whole thing should be redesigned from scratch[2] so it doesn't seem worth it to break things only to break them again shortly after.

[2] A related discussion and an idea floating around is to build something on top of OCaml's odoc.

lyxia boosted
lyxia boosted

Proving Algebraic Datatypes are “Algebraic” in #Coq

It was fun to write, hope you enjoy reading it. I tried to spellcheck it, but tbh I wouldn’t be surprise to find mistakes… If you notice some, feel free to tell me!

woohoo, 4h to the deadline, arguing with coauthors about whether a proof is correct (luckily entirely nonessential either way)...

lyxia boosted

I’ve finally started to work on my next blogpost: Why algebraic datatypes are “algebraic,” explained.

Inspired by @na and her nice write-up (in French, here

Proofs are done[§], I need to actually write the explanation now x).


lyxia boosted
lyxia boosted

Goldman's new "free" typeface has a license that prevents you from using it to criticize Goldman Sachs.


lyxia boosted

HTTP status emojis:

- 200 👍
- 201 🆕
- 301 👉
- 400 👎
- 401 🔒
- 402 💰
- 403 🚫
- 404 🤷‍♂️
- 408 ⌛️
- 410 💨
- 418 🍵
- 500 💩

(via francesc)

lyxia boosted

Il y a deux types d'escargots : les escargots avec habitat, et les escargots sans habitat… Mais ceux-là, on les appelle des limaces.

Parmi les escargots avec habitat, il y a deux types d'escargots : les escargots sans rayures, et les escargots avec rayures… Mais ceux-là, on les appelle des berlingots.

Cependant, nous distinguons les escargots avec habitat sans rayure sphériques, des escargots avec habitat sans rayure non sphériques. Mais ceux-là on les appelle des galets.

Il faut noter qu'il existe deux types de berlingots : les berlingots lévogyres et les berlingots dextrogyres… Mais ceux-là on les appelles des sucettes.

Nous vous devons de vous informer que nous distinguons deux types de galets : les galets blancs et les galets jaunes… Mais ceux-là on les appelle des sablés bretons.

Revenons à nos limaces, il existe deux espèces de limaces : les limaces marrons et les limaces oranges, mais celles-là on les appelle des rustines (aussi appelé chewing gum fruit de la passion).

Parmi les sablés bretons, nous trouvons les sablés bretons sans œuf et les sablés bretons avec œuf… Mais ceux-là, on les appelle omelette.

Il existe deux types d'omelettes : les omelettes bien cuites et les omelettes baveuses. Mais celles-là, on les appelle escargots.


lyxia boosted
lyxia boosted

Vous connaissez un endroit ou les films / séries ont un score en fonction de leur taux de perpétuation des stéréotypes de genre ?

Ça saoule, a force.

Adding more threads slows my program down. 😱

lyxia boosted

9 services en ligne libres, du collectif CHATONS pour télétravailler : rédaction et tableur collaboratifs, partage de fichiers, d'images, visio-conférence, etc.
Parfaitement libres, gratuits, sans inscription et respectueux de votre .

lyxia boosted
lyxia boosted

I've just realized "resumption" and "continuation" are synonymous. I somehow did equate the two subconsciously when reading papers using either words. Now I'm just shocked my subconsciousness did that without telling me.

Nyalas are badly painted antelopes.

Show older
La Quadrature du Net - Mastodon - Media Fédéré est une serveur Mastodon francophone, géré par La Quadrautre du Net.