louisswarren

#!/bin/sh

# Generate all .m4 file outputs - being lazy and just re-running the script
# with an argument. To be safe AND lazy, add a useless argument just to make
# sure this doesn't fork bomb me some day if I change how this is done.
if [ -z "$1" ]; then
	exec find $(dirname -- "$0") -name '*.m4' -exec "./$0" '{}' 'safety' \;
fi

# Generate $1 from its .m4 file.

louisswarren

*.vim
*.agdai

louisswarren

from time import time, sleep

def runtime(f, retcont):
    t = time()
    r = f()
    tt = time()
    if retcont == []:
        retcont.append(r)
    elif retcont is not None:
        assert(r == retcont[0])

louisswarren

from collections import namedtuple
import re

# Literal patterns only match themselves, but quack like regular expressions

class LiteralPattern(str):
    def match(self, other):
        if other.startswith(self):
            return LiteralMatch(str(self))
        return None

louisswarren

CFLAGS = -std=c99 -Wall

main : main.o

.PHONY : test clean

test : main
	./$^ "*regex*" "*vtable*" < main.c

clean :

louisswarren

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>

void print_bin(uint32_t x)
{
	int i;
	for (i = 31; i >= 0; --i)
		putchar(x & (1 << i) ? '1' : '0');
}

louisswarren

arrowelim : {A B : Set} → (A → B) → A → B
arrowelim f a = f a


data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

disjintro₁ : {A : Set} → A → (X : Set) → A ⊎ X
disjintro₁ a X = inl a

louisswarren

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ
{-# BUILTIN NATURAL ℕ #-}


infixl 6 _+_
_+_ : (n m : ℕ) → ℕ
n + zero = n
n + suc m = suc (n + m)

louisswarren

\documentclass[a4paper]{article}
\usepackage{bussproofs}
\usepackage{savetrees}
\usepackage{amsmath}

\newcommand{\using}[2]{\AxiomC{}\RightLabel{#1}\UnaryInfC{#2}}

\newcommand{\assume}[1]{\AxiomC{#1}}
\newcommand{\closed}[2]{\AxiomC{$\left[\text{#2}\right]^\text{#1}$}}

louisswarren

.PHONY: default
default: spectrum.png

.PHONY: waves-video
waves-video: waves
	./$< | mpv --no-correct-pts --fps=30 --scale=oversample -

.PHONY: test test-video
test: nz.png
	sxiv $^