Skip to content

Instantly share code, notes, and snippets.

View poizan42's full-sized avatar

Kasper Fabæch Brandt poizan42

View GitHub Profile
@poizan42
poizan42 / inf-primes.v
Created November 27, 2014 20:08
Proof of the infinitude of primes
Require Import Coq.ZArith.ZArith.
Require Import Coq.ZArith.Znumtheory.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Finite_sets.
Require Import Coq.PArith.BinPos.
Definition Z_ens := Ensemble Z.
Print Finite.
Print Empty_set.
Definition is_empty_set U A := forall x, ~(In U A x).
@poizan42
poizan42 / triangular.v
Created November 11, 2014 21:43
Proof of the closed form formula for triangular numbers
Require Import Coq.Arith.Div2.
Require Import Coq.Arith.Mult.
Require Import Coq.Arith.Even.
Require Import ArithRing.
Fixpoint triangular (n: nat) :=
match n with
| 0 => 0
| S n => (S n) + triangular (n)
end.
(* const : 'a -> 'b -> 'a
* Giver den konstante funktion der giver x. *)
fun const x _ = x
(* Lad os få os en IO monade så vi ikke skal se på alt det urene snask. *)
signature IOSig = sig
type 'a io
(* Monade operationer *)
val >>= : 'a io -> ('a -> 'b io) -> 'b io
val >> : 'a io -> 'b io -> 'b io

Keybase proof

I hereby claim:

  • I am poizan42 on github.
  • I am poizan42 (https://keybase.io/poizan42) on keybase.
  • I have a public key whose fingerprint is 66C6 C343 F614 65F9 248E 204E B00A C5E2 7BCE D2B8

To claim this, I am signing this object:

@poizan42
poizan42 / wolf128.sml
Last active August 29, 2015 14:06
SML port of the 128-byte raytracer wolf128. See http://finalpatch.blogspot.dk/2014/06/dissecting-128-byte-raycaster.html. Uses the InstagraML library: https://github.com/DIKU-IP/InstagraML
(* ex: set ts=2 sw=2 et ai: *)
use "InstagraML.sml";
local
fun rayMarch (x,y,z) =
let
val xdist0 = (((x-160) * z + 4096) div 256) mod 256
val ydist = (((y-100) * z + 4096) div 256) mod 256
val xdist = case z div 64 of
@poizan42
poizan42 / explodeUtf8.sml
Last active September 28, 2018 13:49
UTF-8 decoder in Standard ML
exception Encoding of string;
local
fun decodeUtf8Chars nil = nil
| decodeUtf8Chars (c::rest) =
if c < #"\128" then (ord c)::(decodeUtf8Chars rest)
else
let
val cn = ord c
(* 0xF4 is the largest allowed start byte after the restriction
<?php
class MySQLException extends Exception
{
private $errNo;
private $errStr;
public function __construct($message = null, $errNo = null, $errStr = null)
{
$this->message = $message;
$this->errNo = $errNo;
@poizan42
poizan42 / get-undelivered-list.py
Created May 27, 2014 09:15
Script which generates a json formatted list of email adresses and reasons from bounce mails loaded from an imap account
#!/usr/bin/env python
import imaplib
import email
import json
import re
from getpass import getpass
label = "undelivered-mails"
username = "user@gmail.com"
addrfilename = 'failed-addresses.txt'
using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
namespace CCITTFaxFileScan
{
class Program
@poizan42
poizan42 / StreamTools.cpp
Last active August 29, 2015 13:56
ClrHacks. Kids, don't try this at home.
// StreamTools.h
#pragma once
#include "StdAfx.h"
using namespace System;
using namespace System::IO;
using namespace System::Runtime::InteropServices;