View mfwpp
#!/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. |
View .gitignore
*.vim | |
*.agdai |
View bench.py
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]) |
View lexer.py
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 |
View Makefile
CFLAGS = -std=c99 -Wall | |
main : main.o | |
.PHONY : test clean | |
test : main | |
./$^ "*regex*" "*vtable*" < main.c | |
clean : |
View threeand.c
#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'); | |
} |
View natded.agda
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 |
View agda.agda
data ℕ : Set where | |
zero : ℕ | |
suc : (n : ℕ) → ℕ | |
{-# BUILTIN NATURAL ℕ #-} | |
infixl 6 _+_ | |
_+_ : (n m : ℕ) → ℕ | |
n + zero = n | |
n + suc m = suc (n + m) |
View natded.tex
\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}$}} |
View Makefile
.PHONY: test test-video | |
test: nz.png | |
sxiv $^ | |
test-video: fire | |
./fire | mpv --no-correct-pts --fps=30 --scale=oversample - | |
%.png: %.ppm | |
convert $< $@ |
NewerOlder