Skip to content

Instantly share code, notes, and snippets.

Louis Warren louisswarren

Block or report user

Report or block louisswarren

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@louisswarren
louisswarren / stdouttofile.py
Created Dec 9, 2019
Redirect stdout to a file in python using with block
View stdouttofile.py
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
louisswarren / Graph.agda
Last active Nov 27, 2019
Graphs in agda
View Graph.agda
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
louisswarren / pips.py
Created Nov 18, 2019
Graph sequence thing
View pips.py
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
louisswarren / obviously.py
Created Nov 6, 2019
Decorator for adding obvious assertions to functions
View obviously.py
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
louisswarren / 2019-10-11.md
Last active Oct 15, 2019
Daily logging made easier with a simple python script
View 2019-10-11.md

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
louisswarren / openstd.py
Created Oct 8, 2019
Python open which uses a hyphen for stdin and stdout
View openstd.py
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
louisswarren / closure.agda
Last active Sep 23, 2019
Closure (hull) operators in agda
View closure.agda
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
louisswarren / openmenu.sh
Last active Sep 2, 2019
Dmenu is amazing
View openmenu.sh
#!/bin/sh
cd ~
files=$(find * -not -path "*/.git/*" -not -name "*.agdai")
choice=$(echo "$files" | dmenu -i -p "xdg-open" $@)
xdg-open "$choice"
@louisswarren
louisswarren / tt.agda
Last active Sep 6, 2019
Type theory chapter of the HoTT book in Agda
View tt.agda
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
View Decidable.agda
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)
You can’t perform that action at this time.