skaslev

from sys import stdout
from primefac import primefac
from math import sqrt

# -- "any sufficiently well-commented lisp program contains an ML program in its comments"
# def solution (p a b : N) := a^2 + b^2 = (ab + 1) p^2
# def sym (p a b : N) : solution p a b -> solution p b a
# def sol0 (p : N) : solution p 0 p
# def generator (p a b : N) (p > 0) (a <= b) : solution p a b -> solution p b (b * p^2 - a)

skaslev

open eq

inductive I (F : Type₁ → Prop) : Type₁ :=
mk : I F

axiom InjI : ∀ {x y}, I x = I y → x = y

definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).

definition p := I P

skaslev

/**
 * Sobol Noise Generation
 *	GNU LGPL license
 *	By Dr. John Burkardt (Virginia Tech)
 * https://gist.github.com/alaingalvan/af92ddbaf3bb01f5ef29bc431bd37891
 */

//returns the position of the high 1 bit base 2 in an integer n
int getHighBit1(int n)
{

skaslev

// Ray Tracing Gems Chapter 25
// Code provided by Electronic Arts
// Colin Barré-Brisebois, Henrik Halén, Graham Wihlidal, Andrew Lauritzen,
// Jasper Bekkers, Tomasz Stachowiak, and Johan Andersson
// Errata corrected by Alain Galvan

struct HaltonState
{
    unsigned dimension;
    unsigned sequenceIndex;

skaslev

#include "buf.h"
#include "die.h"

void buf_do_realloc_(void **a, size_t nr, size_t sz)
{
	struct buf *b;

	b = realloc(buf_get_(*a), offsetof(struct buf, data) + nr * sz);
	if (!b)
		die_errno("realloc");

skaslev

Effective Modern CMake

Getting Started

For a brief user-level introduction to CMake, watch C++ Weekly, Episode 78, Intro to CMake by Jason Turner. LLVM’s CMake Primer provides a good high-level introduction to the CMake syntax. Go read it now.

After that, watch Mathieu Ropert’s CppCon 2017 talk Using Modern CMake Patterns to Enforce a Good Modular Design (slides). It provides a thorough explanation of what modern CMake is and why it is so much better than “old school” CMake. The modular design ideas in this talk are based on the book [Large-Scale C++ Software Design](https://www.amazon.de/Large-Scale-Soft

skaslev

-- f(x) = x + f(g(x)) ↔ f(x) = Σ n:ℕ, gⁿ(x)
inductive F (g : Type → Type) : Type → Type 1
| F0 : Π {α}, α → F α
| F1 : Π {α}, F (g α) → F α

-- g(x) = x + x g(x) ↔ g(x) = x/(1-x) ↔ gⁿ(x) = x/(1-nx)
inductive G α : Type
| G0 : α → G
| G1 : α → G → G

skaslev

def algebraic (I : Type) (J : I → Type) (K : Π i : I, J i → Type) :=
Σ i : I, Π j : J i, K i j

inductive F₁
| e₀ : F₁

inductive F₂
| e₀ : F₂
| e₁ : F₂

skaslev

namespace cat
universes u v

@[class] structure category :=
  (obj : Type u)
  (hom : obj → obj → Type v)
  (cid : ∀ {x : obj}, hom x x)
  (comp : ∀ {x y z : obj}, hom y z → hom x y → hom x z)
  (assoc : ∀ {x y z w} {f : hom x y} {g : hom y z} {h : hom z w},
    comp h (comp g f) = comp (comp h g) f)

skaslev

def ran (g h : Type → Type) (α : Type) := Π β, (α → g β) → h β
def lan (g h : Type → Type) (α : Type) := Σ β, (g β → α) × h β

def mapr {g h} {α β} (s : α → β) (x : ran g h α) : ran g h β :=
λ b t, x b (t ∘ s)

def mapl {g h} {α β} (s : α → β) (x : lan g h α) : lan g h β :=
⟨x.1, ⟨s ∘ x.2.1, x.2.2⟩⟩

attribute [reducible] id