louisswarren

import sys

class stdout_to_file:
    def __init__(self, f):
        self.f = f
        self.stdout = sys.stdout

    def __enter__(self):
        sys.stdout = self.f

louisswarren

module Graph where

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

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

len : {A : Set} → List A → ℕ

louisswarren

def run(G, n):
    for _ in range(n):
        i = len(G[0]) - 1
        for j in range(len(G)):
            s = 0
            if 0 <= j - 1:
                s += G[j - 1][i]
            if j + 1 < len(G):
                s += G[j + 1][i]
            G[j] += (s, )

louisswarren

def obviously(v, msg=''):
    def outer(f):
        def inner(*args, **kwargs):
            r = f(*args, **kwargs)
            if not v(r):
                if msg:
                    errmsg = f.__name__ + ': ' + msg
                else:
                    errmsg = f.__name__ + ': obviously not true'
                raise Exception(errmsg)

louisswarren

Friday 11th October 2019

A typical Friday

Keywords: logging, programming, overcast

I made a simple script for writing daily logs. This could be useful for taking notes regarding daily progress. This could have been valuable while doing my PhD. Oh well.

The weather isn't great today. Not terrible, just not great.

louisswarren

import sys

def openstd(file, mode='r', *args, **kwargs):
    if file == '-':
        if 'r' in mode:
            return sys.stdin
        elif any(w in mode for w in 'wxa'):
            return sys.stdout
        else:
            raise Exception("Mode not supported")

louisswarren

open import Agda.Primitive

Pred : ∀{a} → Set a → Set _
Pred A = A → Set

_∈_ : ∀{a} {A : Set a} → A → Pred A → Set
x ∈ α = α x

_⊂_ : ∀{a} {A : Set a} → Pred A → Pred A → Set a
α ⊂ β = ∀ x → x ∈ α → x ∈ β

louisswarren

#!/bin/sh
cd ~
files=$(find * -not -path "*/.git/*" -not -name "*.agdai")
choice=$(echo "$files" | dmenu -i -p "xdg-open" $@)
xdg-open "$choice"

louisswarren

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

Π : ∀{a b} → (A : Set a) → (B : A → Set b) → Set (a ⊔ b)
Π A B = (x : A) → B x

syntax Π A (λ x → B) = Π[ x ∶ A ] B


record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where

louisswarren

open import Agda.Builtin.Equality public

data ⊥ : Set where

¬_ : (A : Set) → Set
¬ A = A → ⊥

infix 4 _≢_
_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬(x ≡ y)