bergwerf

type Array_Element<A> = A extends (infer T)[] ? T : never

type Fixed_Array<A, X> =
  [A] extends [[]] ? [] :
  [A] extends [[X, ...infer T]] ? [X, ...Fixed_Array<T, X>] : never

type Vector<V> = Fixed_Array<V, Vector_Car<V>>
type Vector_Car<V> = [V] extends [number[]] ? number : Vector<Array_Element<V>>

class Vec<V extends Vector<V>> {

bergwerf

// Based on https://github.com/alexei/sprintf.js
//
// Copyright (c) 2007-present, Alexandru Mărășteanu <[email protected]>
// All rights reserved.
// 
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are met:
// * Redistributions of source code must retain the above copyright
//   notice, this list of conditions and the following disclaimer.
// * Redistributions in binary form must reproduce the above copyright

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.