Other articles

  1. Thunderlink on macOS

    Thunderlink is a fantastically useful add-on for the Thunderbird mail user agent. It lets you create links to email that you can put into all sorts of documents (like ToDo lists or notes). The links use the URI scheme thunderlink that needs to be handled by whatever mechanism you use …

    read more
  2. Make Firefox play embedded MP4 videos

    Date: 2015-01-03

    Tags: tools

    For some reason (at least on Mac OS X and according to a quick search also on other platforms) Firefox does not play MP4 videos embedded into websites using the <video> tag. Seems that enabling the two config options media.fragmented-mp4.enabled and media.fragmented-mp4.exposed fixes the issue.

    Configuring Firefox to enable playing embedded MP4 videos

    read more
  3. vim-like ctrl+v enter in Emacs

    Date: 2012-12-17 (updated: 2022-09-21)

    Tags: tools

    Suppose you have a list like this

    foo, bar, baz, quux

    in your Emacs buffer, but you’d rather have one element per line like this


    What to do? In vim this is easy:


    where ^M is inserted using


    But what …

    read more
  4. Thunderbird line breaking behaviour

    Because I keep forgetting which options to set to force Thunderbird to send and display line breaks instead of flowed plain text emails that may or may not come out right at the other end (usually those emails exhibit unsightly long lines which among other things might make quoting from …

    read more
  5. Snippets for LaTeX + Emacs users

    I've been using Emacs to edit LaTeX for some time now, mostly resorting to AUCTeX#s keyboard commands to insert fonts, environments and some other stuff that I need in some documents. But I'm also a big fan of yasnippet, the de facto standard for inserting more or less complex …

    read more
  6. Several ways to prove a simple proposition

    Date: 2011-02-17

    Tags: coq

    Coq provides many tactics. In this post we show a number of proofs that use different tactics to prove a simple proposition of first order logic, namely \(\forall P\;Q,\, P \wedge Q \rightarrow Q \wedge P\) which in Coq translates to

    forall P Q : Prop, P /\ Q -> Q /\ P …
    read more
  7. Using Qucs for filter design

    Qucs, short for Quite Universal Circuit Simulator, is as the name suggests a simulation package for electronic circuits. It's free and sports a nice graphical schematic capture interface. One of its many nice and useful features is the ability to write equations so you can calculate all kinds of stuff …

    read more
  8. Beginning Ltac

    Date: 2011-02-10

    Tags: coq

    One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language \(\mathcal{L}_{tac}\). Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, we can simply write down new tactics …

    read more
  9. How to draw commutative diagrams in LaTeX with TikZ

    Sooner or later everyone who uses LaTeX to typeset documents containing maths will encounter the problem of how to draw commutative diagrams. There are many packages, some general purpose other specialized for the task. An excellent survey of some of these alternatives by James Milne can be found here.

    I …

    read more
  10. Another script font for LaTeX

    Sometimes it’s nice to have an extra script font available to make distinctions between different kinds of objects clearer. One such font is Ralph Smith’s Formal Script (see here for the TeX Catalogue entry) which is provided by the mathrsfs package.

    This gives you a new LaTeX font …

    read more
  11. The Maybe monad in Coq

    The Maybe monad is pretty useful whenever you're dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.

    The first idea is a to lift the codomain of a partial function \(f : A \rightharpoonup …

    read more