miikka

#!/usr/bin/env python
# Like sleep(1), but shows a spinner while waiting.

import time
import sys

CHARS = '/-\\|'


def spin(delay):

miikka

/* We present: high-quality highly accurate nanosleep with a spinner.
 *
 * Compile and run:
 * 
 *     gcc -shared -fPIC -o libsleep.so sleep.c
 *     LD_PRELOAD=./libsleep.so sleep 3
 * */

#include <time.h>

miikka

/* Recursively observe property reads of an object. 
 *
 * Takes the target and an object for returning results. Returns the proxied
 * target. Results are assigned to result.reads.
 *
 * Example:
 *
 *     var target = {a: 1};
 *     var result = {};
 *     target = observeReads(target, result);

miikka

# RELAX NG compact syntax cheat sheet

# See also:
# * tutorial <http://www.relaxng.org/compact-tutorial-20030326.html>
# * spec <http://www.relaxng.org/compact-20021121.html>

# Checking a XML file:
#
#     jing -c schema.rnc file.xml
#

miikka

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.

miikka

import string

from lxml import etree
from lxml.etree import QName
from lxml.builder import E

from hypothesis import strategies as st

NS = "http://relaxng.org/ns/structure/1.0"

miikka

from collections import defaultdict, namedtuple
import numpy as np

def visible_cap_central_angle(altitude):
    earth_radius = 6371.0
    return np.arctan2(np.sqrt(altitude * (altitude + 2 * earth_radius)),
                      earth_radius)

def hav(x):
    return np.sin(x/2)**2

miikka

(ns example
  (:require [clojure.spec :as spec]
            [ring.swagger.swagger2 :as rs]
            [schema.core :as s]))

(spec/def ::id string?)
(spec/def ::name string?)

(spec/def ::street string?)
(spec/def ::city #{"tre" "hki"})

miikka

#!/usr/bin/env python
# Inspired by this tweet: https://twitter.com/AtticusBones/status/787936821892317184

from __future__ import division

import atexit
import curses
import math
import random
import sys

miikka

Axiom a1 : forall A B, A -> (B -> A).
Axiom a2 : forall A B, (~B -> ~A) -> (A -> B).

Theorem dne :
  forall A, ~~A -> A.
Proof.
  intros A P.
  generalize P.
  apply a2, a2, a1, P.
Qed.