: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

@TheAspiringHacker
Yeah it's really more of a full build system, quite overkill for just blogging.

lyxia boosted

@lthms
I'm pretty sure all it takes is just starting something, but as always people are busy.

@lthms
Although I have no idea what documentation in Coq should look like to account for dependent types.

@lthms
I would also really like to work on that!

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 

@amiloradovsky @lthms It boils down to the idea that proofs are a means to an end, whether that is ruling out bad programs or improving our understanding of the world. And we should always be critical of how our means meet our ends.

@amiloradovsky @lthms There are steps we can take to ensure a relation we defined is not too trivial, such as proving that it correctly distinguishes certain classes of examples, or that it implies some other result which we are more confident is nontrivial.

@epicmorphism
@lthms
Indeed, although it's really a hard sell compared to the convenience of Leibniz equality.

lyxia boosted

I am doing it anyway鈥 and it鈥檚 funny to rework on my article about generalized rewriting two years later.

If I鈥檝e 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.

Show more
niu.moe

Welcome to your niu world ! We are a cute and loving international community 锛(鈮р柦鈮)锛 !