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
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)
@louisswarren
louisswarren / bloomheap.py
Last active Jul 20, 2019
Min heap using a tape of booleans
View bloomheap.py
# Idea suggested by Michael Cowie
import itertools
class BloomHeap:
def __init__(self, *values):
self.tape = []
if len(values) == 1 and not isinstance(values[0], int):
self += values[0]
elif values:
View 28.py
days = ['Monday', 'Tuesday', 'Wednesday',
'Thursday', 'Friday', 'Saturday', 'Sunday']
def time(n):
day = days[(n // 24) % 7]
n = n % 24
if n == 0:
hour = '12am'
elif n < 12:
hour = f'{n}am'
elif n == 12:
@louisswarren
louisswarren / disease.py
Created Jul 15, 2019
Basic disease modelling in python
View disease.py
from random import random, sample
import networkx as NX
import numpy as NP
from matplotlib import pyplot as MPL
class Graph:
def __init__(self, vertices, edges):
self.vertices = vertices
self.edges = edges
@louisswarren
louisswarren / arrow.agda
Created Jul 2, 2019
Decidability for the implicational fragment in Agda
View arrow.agda
module Logic (X : Set) where
open import Decidable
open import List
--infixr 5 _++_
--_++_ : {A : Set} List A List A List A
--[] ++ ys = ys
--(x ∷ xs) ++ ys = x ∷ xs ++ ys
@louisswarren
louisswarren / logging.py
Last active Jun 25, 2019
Logging in python, because mutable default arguments is a feature
View logging.py
def log(x=None, acc=[]):
if x is None:
print('\n'.join(acc))
else:
acc.append(x)
log("Hello")
log("Goodbye")
log()
@louisswarren
louisswarren / implicational.py
Last active Jun 15, 2019
Decidability algorithm for the implicational fragment of minimal logic
View implicational.py
# Simple implementation of proving/disproving implicational statements
from collections import namedtuple
# String constants
lBOT = ''
lNEG = '¬'
lIMP = ''
lMMP = ''
@louisswarren
louisswarren / siso.py
Created Jun 10, 2019
Python co-routine to store a single value
View siso.py
from collections import namedtuple
Arrow = namedtuple('Arrow', 'tail head')
# Single input single output
def siso():
def inner():
x = yield
yield
yield x
@louisswarren
louisswarren / possum.py
Last active May 28, 2019
Simulate possums meeting on random walks in python
View possum.py
import random
class Point:
def __init__(self, x, y):
self.x = x
self.y = y
def __add__(self, other):
return Point(self.x + other.x, self.y + other.y)
@louisswarren
louisswarren / lagdastrip.py
Last active Jun 1, 2019
Strip literate agda down to agda
View lagdastrip.py
#!/usr/bin/env python3
import sys
def get_code_lines(lines):
in_code = False
for line in lines:
if line.startswith(r'\begin{code}'):
in_code = True
yield '--STRIP: '
You can’t perform that action at this time.