louisswarren

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

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

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

def log(x=None, acc=[]):
    if x is None:
        print('\n'.join(acc))
    else:
        acc.append(x)

log("Hello")
log("Goodbye")
log()

louisswarren

# Simple implementation of proving/disproving implicational statements

from collections import namedtuple

# String constants

lBOT = '⊥'
lNEG = '¬'
lIMP = ' → '
lMMP = ' ⇒ '

louisswarren

from collections import namedtuple

Arrow = namedtuple('Arrow', 'tail head')

# Single input single output
def siso():
    def inner():
        x = yield
        yield
        yield x

louisswarren

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

#!/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: '

louisswarren

open import Agda.Builtin.Float

record Colour : Set where
  constructor colour
  field
    r g b : Float
    

louisswarren

data ⊥ : Set where

hmm : ∀ α → ⊥
-- Agda infers that
--   α : ⊥
-- because that's only way this could be provable?
hmm α = α