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

Python Proposals

cast decorator

The common python pattern

def foo():
    tmp = []
from collections import namedtuple
from enum import Enum
import random
compose = lambda f: lambda g: lambda *a, **k: f(g(*a, **k))
class Face(Enum):
ACE = 'A'
TWO = '2'

ffmpeg notes

I often want to do something that I believe is non-trivial in ffmpeg, only to discover that it is actually very simple, if only I had known how to do it. I even end up writing wrappers to do simple things, because I keep forgetting what to do. However, this file is my new solution: simply write my own documentation for things I would occasionally like to do.

import heapq
class Task:
def __init__(self, time):
self.time = time
def __lt__(self, other):
return self.time < other.time
def __repr__(self):
louisswarren /
Last active Mar 13, 2020
Spite in python
import curses
BOX = {
'light': ('┌───┐',
'│ │',
'│ │',
'heavy': ('┏━━━┓',
louisswarren /
Last active Mar 7, 2020
Menus with curses in python
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) = curses.newwin(self.height + 2, self.width + 8, y, x)
louisswarren / bug-2-6-1.agda
Last active Feb 24, 2020
Bug in Agda version
View bug-2-6-1.agda
-- Agda version
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma
ℕ×ℕ : Set
ℕ×ℕ = Σ ℕ λ _
record Cont : Set where
louisswarren /
Last active Feb 20, 2020
List all of the days in a given year
if [ "$1" = "--help" ] || [ $1 = "-h" ]; then
echo "Usage: listdays [year] [format]"
if [ -n "$1" ]; then
year=`date "+%Y"`
louisswarren / wtype.agda
Last active Jan 29, 2020
W-types in agda
View wtype.agda
-- Based on
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 / 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_ :
You can’t perform that action at this time.