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 task.py
import heapq
class Task:
def __init__(self, time):
self.time = time
def __lt__(self, other):
return self.time < other.time
def __repr__(self):
@louisswarren
louisswarren / spite.py
Last active Mar 13, 2020
Spite in python
View spite.py
import curses
SPADE, HEART, DIAMOND, CLUB = '♠♥♦♣'
BOX = {
'light': ('┌───┐',
'│ │',
'│ │',
'└───┘'),
'heavy': ('┏━━━┓',
@louisswarren
louisswarren / cursesexample.py
Last active Mar 7, 2020
Menus with curses in python
View cursesexample.py
import curses
class Menu:
def __init__(self, y, x, options):
self.y = y
self.x = x
self.options = options
self.height = len(options)
self.width = max(len(opt) for opt in options)
self.win = curses.newwin(self.height + 2, self.width + 8, y, x)
@louisswarren
louisswarren / bug-2-6-1.agda
Last active Feb 24, 2020
Bug in Agda version 2.6.0.1.20191219
View bug-2-6-1.agda
-- Agda version 2.6.0.1.20191219
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma
ℕ×ℕ : Set
ℕ×ℕ = Σ ℕ λ _
record Cont : Set where
@louisswarren
louisswarren / listdays.sh
Last active Feb 20, 2020
List all of the days in a given year
View listdays.sh
#!/bin/sh
if [ "$1" = "--help" ] || [ $1 = "-h" ]; then
echo "Usage: listdays [year] [format]"
exit
fi
if [ -n "$1" ]; then
year="$1"
else
year=`date "+%Y"`
@louisswarren
louisswarren / wtype.agda
Last active Jan 29, 2020
W-types in agda
View wtype.agda
-- 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
louisswarren / lift.agda
Last active Jan 10, 2020
Lift types by instance resolution in Agda
View lift.agda
data : Set where
zero :
suc :
data : Set where
nonneg :
negsuc :
data : Set where
frac_/suc_ :
@louisswarren
louisswarren / Discrete.agda
Last active Dec 18, 2019
Instance resolution for decidable equality of discrete types
View Discrete.agda
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
louisswarren / basic.agda
Created Dec 16, 2019
A basic imperitive language in agda
View basic.agda
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
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
You can’t perform that action at this time.