louisswarren

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.

louisswarren

import heapq

class Task:
    def __init__(self, time):
        self.time = time

    def __lt__(self, other):
        return self.time < other.time

    def __repr__(self):

louisswarren

import curses

SPADE, HEART, DIAMOND, CLUB = '♠♥♦♣'

BOX = {
    'light':       ('┌───┐',
                    '│   │',
                    '│   │',
                    '└───┘'),
    'heavy':       ('┏━━━┓',

louisswarren

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

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

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

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

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data ℤ : Set where
  nonneg : ℕ → ℤ
  negsuc : ℕ → ℤ

data ℚ : Set where
  frac_/suc_ : ℤ → ℕ → ℚ

louisswarren

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

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