louisswarren

-- Based on https://mazzo.li/epilogue/index.html%3Fp=324.html

data W (S : Set) (P : S → Set) : Set where
  _◁_ : (s : S) → (P s → W S P) → W S P

data 𝟘 : Set where

data 𝟙 : Set where
  ● : 𝟙

louisswarren

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data ℤ : Set where
  nonneg : ℕ → ℤ
  negsuc : ℕ → ℤ

data ℚ : Set where
  frac_/suc_ : ℤ → ℕ → ℚ

louisswarren

module Discrete where

open import Agda.Builtin.Equality public

data ⊥ : Set where

¬_ : ∀{a} → Set a → Set a
¬ A = A → ⊥

data Dec {a} (A : Set a) : Set a where

louisswarren

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

Num = ℕ

record Var : Set where
  constructor var
  field
    idx : ℕ

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")