~lthms @lthms@mastodon.social
I don’t like syntax highlighting.
Joined Apr 2017
Pinned toot
My better half, genuinely : “Oh right, you’re old, you don’t know that.
Pinned toot
Hardware? It’s just someone else’s software
Eh, Masto, je me posais une question.
Il se passe quoi quand un streamer affilié se fait ban de #Twitch pendant 2 semaines ? Est-ce que Twitch lui verse les revenus de ses abonnements à la fin du mois comme si de rien était ?
Ltac can be used to do fun tricks, like computing the type of a fold function for any given datatype, as long as we can provide the “canonical form” (like unit + a * list a for lists)
https://gist.github.com/lthms/1802b29ea4b3afa06ca625808da19ebc
And… non_empty_list α == α * list α
This one was tricky to prove (I wanted to prove it by rewriting, but couldn’t ): )
Another nice lemma to prove :
α * (β + γ) == α * β + α * γ.
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 https://blog.gelez.xyz/type-produit/)
Proofs are done[§], I need to actually write the explanation now x).
[§]: https://gist.github.com/lthms/8f93f3c4b9527b97997cada2a05b8902
~lthms
boosted
Common lisp
Uncommon lisp
Rare lisp
Epic lisp
Legendary lisp
Eh @raichoo (: I don’t know if you have a lobste.rs account, but you may be interested in the comments of this submission :p
https://lobste.rs/s/vohztm/hikari_wayland_compositor
(if you want an invit, feel free to ask for one!)
~lthms
boosted
This worked... I'm slightly surprised. https://gist.github.com/edwinb/79186fd23c26e8ca030577ebb35c6967
(It's an echo server, with the socket state tracked via linear socket types.)
Stories? LinkedIn? Wtf?
(I don’t have a LinkedIn account, I’m just curious)
~lthms
boosted
~lthms
boosted
Introducing the BARE message encoding
https://drewdevault.com/2020/06/21/BARE-message-encoding.html
You know the feeling when everything happens in three days, so you can’t do anything today?
Coq 8.12+beta1 has been tagged! Happy beta testing. (: https://github.com/coq/coq/releases
~lthms
boosted
Ça me fait penser, je ne sais plus si je l’ai dit ici, mais ma bibliothèque #Coq pour les politiciens est disponible ici : https://github.com/Mbodin/coq-alternative-facts À utiliser à vous risques et périls !
(Et c’est probablement la seule fois où je suis à peu près sûr que la IGNUTILE est la bonne licence à utiliser.)
RFC: Introduce the guard/unguard attributes for Fixpoint (#Coq)
https://github.com/coq/coq/pull/12539
Would love to have some feedback on this one.
~lthms
boosted
Regardez ce qui vient d'arriver par la poste ! 💕🤩
#poleDance #maVieEnEquilibre #2020bd #mastoart #maPremiereBd #fierté #empoweringwomen #aerial #poletutorial #romangraphique #graphicnovels #glenat
~lthms
boosted
Du coup j'ai un blog
Et j'ai fait un super article d'intro https://blog.gelez.xyz/lancement-du-blog/
Voilà, voilà. Avec un peu de chance je posterais un peu plus que deux articles avant de l'oublier 😬
Kipo ❤️
I don’t like syntax highlighting.
Joined Apr 2017
Server run by the main developers of the project 
It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!