bergwerf

@mixin droplet($color, $time, $size, $scale) {
  position: relative;

  &::after {
    content: '';
    display: inline-block;
    width: $size;
    height: $size;
    border-radius: $size;
    background: $color;

bergwerf

import io
import json
import http.server
import socketserver

HOST = "localhost"
PORT = 8080

class AnalyzerHandler(http.server.BaseHTTPRequestHandler):
  def do_POST(self):

bergwerf

// Try on: https://www.shadertoy.com/new
// With: https://github.com/andrewhills/ShadertoyCustomTextures

// https://www.shadertoy.com/view/XljGzV
vec3 hsl2rgb( in vec3 c )
{
    vec3 rgb = clamp( abs(mod(c.x*6.0+vec3(0.0,4.0,2.0),6.0)-3.0)-1.0, 0.0, 1.0 );
    return c.z + c.y * (rgb-0.5)*(1.0-abs(2.0*c.z-1.0));
}

bergwerf

Require Import Utf8 Nat PeanoNat Lia Compare_dec.
Import Nat.

Section Pigeons.

Variable f : nat -> nat.
Variable Σ N : nat.
Hypothesis bound : ∀i, i < N -> f i < Σ.
Hypothesis overflow : Σ < N.

bergwerf

; http://morphett.info/turing/turing.html

0 * * l start1

start1 * _ l start2
start2 * 1 l start3
start3 * _ l start4
start4 * 1 r first1

first1 _ _ r first2

bergwerf

package main

import "fmt"

type tm struct {
	halt int
	states []state
}

type trans struct {

bergwerf

(* Examples of co-induction, quotient types (setoid), custom termination *)

Require Import Coq.Init.Nat.
Require Import Coq.Unicode.Utf8.
Require Import Coq.Arith.Mult.
Require Import Coq.Arith.Compare_dec.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import Coq.micromega.Lia.
Import PeanoNat.Nat.

bergwerf

Require Import Coq.Lists.List.
Require Import Coq.micromega.Lia.
Import ListNotations.
Arguments In {_}.

Lemma problem N (P : nat -> Prop) (Q : nat -> nat -> Prop) :
  (forall n : nat, P n -> n <= N) ->
  (forall n : nat, n <= N -> exists x, Q n x) ->
  exists l : list nat, forall n, P n -> exists x, In x l /\ Q n x.
Proof.

bergwerf

(* Spread and fan prefix intersections. *)

From intuitionism Require Import lib set seq bcp spr fan.

(* Finite sequence comparison. *)
Section FiniteCompare.

(* Check if two sequences have a shared prefix. *)
Fixpoint fcompare (s t : fseq) := 
  match s, t with

bergwerf

(* The Collatz conjecture, to illustrate reckless statements. *)
Section Collatz.

(* Collatz mapping. *)
Definition collatz_map n := if even n then div2 n else n*3+1.

(* Collatz sequence starting with n. *)
Fixpoint collatz_seq n i :=
  match i with