Mercerenies

#!/bin/bash

# Final script for my way-too-deep analysis of a minigame in Yoshi's Island.
#
# For context, see my blog: http://mercerenies.sdf.org/blog/roulette.php

apl.js <<APL | sed 'y/¯/-/' | gnuplot -e 'set xlabel "Wager"; set ylabel "E"; set terminal png; set output "yoshis_island.png"; plot "-"'

norm←⊢÷(+/)

Mercerenies

// Enjoy my mess of C and C++ style programming. I wrote this in
// Haskell first, but it was too slow, so I decided to make a mess of
// everything and do the memory management myself, which resulted in
// this surprisingly fast version. But I'm too lazy to emulate the
// std::vector sort of stuff in pure C, so I cheated here and there
// when there wasn't a bottleneck.
//
// Anyway, for digit counts from 1 to 11 (where the last digit is
// *always* the "distinct numbers" digit), this prints out every fixed

Mercerenies

% Sadly, GitHub doesn't seem to support syntax highlighting for
% Potassco :(
%
% There's an Emacs mode for it if you want to see this file pretty.
% See the Perl script below for instructions on how to run this.

ispos(1..N) :- length(N).

isdigit(0..N) :- length(N).

Mercerenies

Field Access in Python

This page is an attempt to describe the following Python expression.

foo.bar

It's surprisingly complicated exactly what happens behind the scenes when you access a field on a Python object. And I've written several StackOverflow answers summarizing different parts of this process. But I've never seen a canonical description of the entire process in one place. This page aims to be a one-stop source for what happens when you access a field on a Python object, that people (myself included) can link to in StackOverflow answers as a source for the behavior of Python's complex metaprogramming model.

Mercerenies

-- Proof that my somewhat unusual Biapplicative instance for
-- PredicateZipper is lawful in
-- https://github.com/Mercerenies/lambda-games/blob/master/src/Lambda/Type/Relation.purs

open import Relation.Binary.PropositionalEquality
open import Function

record RawBifunctor (F : Set → Set → Set) : Set₁ where
  field