Skip to content

Instantly share code, notes, and snippets.

Andrej Bauer andrejbauer

Block or report user

Report or block andrejbauer

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@andrejbauer
andrejbauer / mandelbrot.ml
Created Dec 28, 2013
A simple program to compute the Mandelbrot set.
View mandelbrot.ml
(* The Mandelbrot set.
Compile with:
ocamlbuild mandelbrot.native
Example usage:
./mandelbrot.native --xmin 0.27085 --xmax 0.27100 --ymin 0.004640 --ymax 0.004810 --xres 1000 --maxiter 1024 --file pic.ppm
@andrejbauer
andrejbauer / mandelbrot.c
Created Dec 11, 2013
A simple program for computing the Mandelbrot set.
View mandelbrot.c
/*
This program is an adaptation of the Mandelbrot program
from the Programming Rosetta Stone, see
http://rosettacode.org/wiki/Mandelbrot_set
Compile the program with:
gcc -o mandelbrot -O4 mandelbrot.c
Usage:
@andrejbauer
andrejbauer / assoc.elf
Created Jun 18, 2013
Twelf seems very finicky about certain details. Here I explore how associative lists depend in unreasonable ways on the complexity of the value type.
View assoc.elf
% Testing how lookup in an associative list works.
% We consider associative lists with keys of type key and values
% of type value.
%
% Ideally, we want key to be any type with decidable
% equality and value to be any type. However, we use natural numbers
% as keys so that we can convince Twelf that key has decidable equality.
% Is there a way to tell Twelf "assume key has decidable equality"?
%
@andrejbauer
andrejbauer / gist:4272538
Created Dec 12, 2012
A lemma which explains how transport and function extensionalty interact.
View gist:4272538
Variable A : Type.
Variable P : A -> Type.
Variable Q : forall x, P x -> Type.
Lemma transport_funext (f g : forall x, P x) (n : forall x, Q x (f x)) (E : forall x, f x = g x) (x : A) :
(transport (fun h => forall x, Q x (h x)) (funext E) n) x = transport (Q x) (E x) (n x).
You can’t perform that action at this time.