Show more
lyxia boosted
lyxia boosted

Never challenge Death to a pillow fight...

...unless you're prepared to handle the reaper cushions.

What the what. MetaCoq's TemplateMonad is in Prop!?

:blobcatflip: :blobcatcry: :blobcatsweat: trying to write the complete untyped debruijn-indexed syntax tree of a Coq match...

Looking at metacoq (template haskell, except it's coq, and of course it is formalized) reminds me why I'd rather use the GHC.Generics kind of metaprogramming. Semantics, not syntax!

lyxia boosted
@satanya Capitalism: Debt first search
Communism: Bread first search
lyxia boosted
lyxia boosted
lyxia boosted

I really want to get involve in a community effort to give #Coq better documentation tooling.

TIL sha512 is faster than sha256 on 64bit machines and you can see it for yourself with a single command:

openssl speed sha256 sha512

security.stackexchange.com/que

lyxia boosted

insider joke/pun 

lyxia boosted

I am doing it anyway… and it’s funny to rework on my article about generalized rewriting two years later.

If I’ve learned one thing, is that the less vernacular command, the better. So:

1/ Use #[program] instead of Program
2/ Use #[program] Instance _: Equivalence _ instead of Add Parametric Relation
3/ Use #[program] Instance _: Proper (_ ==> _) _ instead of Add Parametric Morphism

I always need to copy/paste when using Add Parametric Relation/Morphism, never with Instance.

lyxia boosted

I am free! Until the next deadline!

lyxia boosted

Unicode subscript digits are a godsend for renaming variables in a compiler IR. The results (lst₀ lst₁ lst₂ etc) are so much more readable than lst_0 lst_1, especially when you have common variable names like x0 y0 x1 y1 ...

lyxia boosted

Je n'ai pas vu passer ça sur le fediverse, malgré la communauté typophile/libriste, alors je partage :
L'ANRT a publié, il y a plus d'un mois, 15 fontes redessinées à partir de documents du XVe siècle, marquant la transitions entre le Gothique et le Romain. C'est sous licence libre !

gotico-antiqua.anrt-nancy.fr/

#design #fonte #typographie #designlibre

lyxia boosted
One day, I'm gonna defect and open a counter instance called vigne.space.

The official documentation for creating a package for , now updated to Opam 2.0: coq.inria.fr/opam-packaging.ht

Show more
niu.moe

Welcome to your niu world ! We are a cute and loving international community O(≧▽≦)O !