louisswarren

open import Agda.Builtin.Nat renaming (Nat to ℕ)

open import List
open import Decidable

data _≤_ : ℕ → ℕ → Set where
  0≤n    : ∀{n} → zero ≤ n
  sn≤sm : ∀{n m} → n ≤ m → (suc n) ≤ (suc m)

_≤?_ : (n m : ℕ) → Dec (n ≤ m)

louisswarren

open import Agda.Primitive
open import Agda.Builtin.Equality

data Chain {n} {A : Set n} (f : A → A) (x : A) : A → Set (lsuc n) where
  nil  : Chain f x x
  link : ∀{y} → Chain f x y → Chain f x (f y)

record FixedPoint {n} {A : Set n} (R : A → A → Set) (f : A → A) : Set (lsuc n) where
  constructor fp
  field

louisswarren

www
ds

louisswarren

DL=wget -O $@

example.pdf: example.tex bin
	pdflatex example.tex

.PHONY: bin
bin: image1.png image2.png

image1.png:
	$(DL) https://....png

louisswarren

import time
import numpy as np
import random

class Layer:
    def __init__(self, weights, biases):
        self.weights = weights
        self.biases = biases

    def breed(self, other):

louisswarren

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma

open import Vec

data Max⟨_,_⟩≡_ : ℕ → ℕ → ℕ → Set where
  maxl : ∀{n} → Max⟨ n    , zero ⟩≡ n
  maxr : ∀{n} → Max⟨ zero , n    ⟩≡ n
  suc  : ∀{n m k} → Max⟨ n , m ⟩≡ k → Max⟨ suc n , suc m ⟩≡ suc k

louisswarren

def tclass(*argnames, then_do=None):
    if len(argnames) == 1 and isinstance(argnames[0], dict):
        argnames = argnames[0]

    def decorator(cls):
        def inner_init(self, *args, **kwargs):
            for argname, arg in zip(argnames, args):
                self.__setattr__(argname, arg)
            for argname in list(argnames)[len(args):]:
                self.__setattr__(argname, argnames[argname])

louisswarren

open import Agda.Builtin.Sigma

ac : {X Y : Set} → (ρ : X → Y → Set) → (∀ x → Σ Y (ρ x)) → Σ (X → Y) (λ φ → ∀ x → ρ x (φ x))
fst (ac ρ rel) x = fst (rel x)
snd (ac ρ rel) x = snd (rel x)

louisswarren

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma
open import Decidable

module Fvec where

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

louisswarren

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl y = y

data Bool : Set where
  False True : Bool