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)

louisswarren

# 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:

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: '