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

louisswarren

import sys

class stdout_to_file:
    def __init__(self, f):
        self.f = f
        self.stdout = sys.stdout

    def __enter__(self):
        sys.stdout = self.f

louisswarren

module Graph where

open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)

data Fin : ℕ → Set where
  zero : ∀{n} → Fin (suc n)
  suc  : ∀{n} → Fin n → Fin (suc n)

len : {A : Set} → List A → ℕ

louisswarren

def run(G, n):
    for _ in range(n):
        i = len(G[0]) - 1
        for j in range(len(G)):
            s = 0
            if 0 <= j - 1:
                s += G[j - 1][i]
            if j + 1 < len(G):
                s += G[j + 1][i]
            G[j] += (s, )

louisswarren

def obviously(v, msg=''):
    def outer(f):
        def inner(*args, **kwargs):
            r = f(*args, **kwargs)
            if not v(r):
                if msg:
                    errmsg = f.__name__ + ': ' + msg
                else:
                    errmsg = f.__name__ + ': obviously not true'
                raise Exception(errmsg)