Show more

Mtac2 looks fun. Exceptions, nontermination, and pattern-matching with arbitrary terms as patterns, in Coq.

lyxia boosted

It looks like selenium is a thing.

Are there tools to keep track of visual changes from and refactoring?

lyxia boosted

@tA @turion
Ookaay... So, I read "15 lines of Bach" at the first glance, and then get stuck for five minutes trying to remember a composer named Haskell.

I just updated the tutorial to "Roll your own bot" on the wiki to use a modern version of the network library. Making bots is a nice way to start learning about networking!

wiki.haskell.org/Roll_your_own

lyxia boosted

Today I completed the secret quest "talk to Matthieu Sozeau" to learn the skill "understand universes (novice)".

This year I'm going to learn how to debug universes inconsistencies. :blobcatread:

lyxia boosted
lyxia boosted
lyxia boosted

TIL, I learnt it is easy to install #Coq beta because there is a special repo for that: core-dev

Have a look at the README if you are interested: github.com/coq/opam-coq-archiv

lyxia boosted
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!

Show more
niu.moe

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