Daily Archives: 2011/01/24

Coq Syntax Highlighting Test

A test case for Coq syntax highlighting in GeSHi (for the WP-Syntax plugin). Inductive nat : Set := | O : nat | S : nat -> nat.   Inductive fin : nat -> Type := | FO : forall … Continue reading

Posted in Coq, Tools | Tagged , , | Leave a comment

Partiality is an effect

In languages like Coq where all computations must terminate and only total functions are allowed it would still be nice to be able to express non-terminating computations. While searching for solutions other people had come up with I stumbled across … Continue reading

Posted in Coq | Tagged , , | Leave a comment

WordPress + SQLite

The one thing that really kept me from just installing WordPress and playing around with it was that it required MySQL to run. I don’t need a full-blown RDBMS on my server and I certainly don’t need MySQL (in the … Continue reading

Posted in Tools | Tagged , , | 4 Comments

How I use git

After many years of using SVN, my current revision control system of choice is git. It makes distributed and offline work a breeze, so I don’t always have to log in in to a remote repository when I want to … Continue reading

Posted in Tools | Tagged , | Leave a comment

Definition of a monad

This rather rendundant post serves as a test case for the WP LaTeX plugin. A monad on a category is given by an endofunctor  and two natural transformations: such that the following two diagrams commute:

Posted in Mathematics | Tagged , | Leave a comment