Silvio Mayolo Mercerenies

## biapply-predicatezipper.agda

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

## FieldAccess.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                Mercerenies
                / FieldAccess.md
            
            
              Last active
              November 6, 2022 00:04
            
          
    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.

  
## selfref.lp

% 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).

## selfref_1.cpp

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

## yoshis_island.sh
#!/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←⊢÷(+/)

## monster_truck_movement.pl
#!/usr/bin/perl

# Insanity in WUAS.

use strict;
use warnings;
use 5.010;

use Data::Dumper;

## mathspiral.html
<!DOCTYPE html>

<html>
  <head>

    <title>Math Stuff for Silly Internet Math Person</title>

    <script type="application/javascript">

     const WIDTH = 320;

## toothpick_game.pl
%% -*- Prolog -*-

% A very simple "toothpicks" game in Prolog. Two players take turns
% drawing one, two, or three toothpicks from a stack. If you take the
% last one, then you lose. I made this late one night, mainly to prove
% to myself that game programming is actually possible in Prolog.

:-
    use_module(library(readutil)).

## silvertongue.pl
#!/usr/bin/perl

use strict;
use warnings;
use 5.010;

=pod

1. B<Don't use big words.> These people aren't very bright. Don't use words longer than 6 characters. Excludes punctuation.

## custom_rules.xml
<?xml version="1.0" encoding="UTF-8"?>
<project name="kotlin_rules">
    <property environment="env"/>
    <typedef resource="org/jetbrains/kotlin/ant/antlib.xml" classpath="${env.KOTLIN_HOME}/lib/kotlin-ant.jar"/>
    <target name="-post-compile">
        <path id="project.javac.classpath">
            <path refid="project.all.jars.path" />
            <path refid="tested.project.classpath" />
            <path path="${java.compiler.classpath}" />
            <path path="${project.target.android.jar}"/>

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

	% 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).

	// 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
	#!/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←⊢÷(+/)
	#!/usr/bin/perl

	# Insanity in WUAS.

	use strict;
	use warnings;
	use 5.010;

	use Data::Dumper;
	<!DOCTYPE html>

	<html>
	<head>

	<title>Math Stuff for Silly Internet Math Person</title>

	<script type="application/javascript">

	const WIDTH = 320;
	%% -- Prolog --

	% A very simple "toothpicks" game in Prolog. Two players take turns
	% drawing one, two, or three toothpicks from a stack. If you take the
	% last one, then you lose. I made this late one night, mainly to prove
	% to myself that game programming is actually possible in Prolog.

	:-
	use_module(library(readutil)).
	<?xml version="1.0" encoding="UTF-8"?>
	<project name="kotlin_rules">
	<property environment="env"/>
	<typedef resource="org/jetbrains/kotlin/ant/antlib.xml" classpath="${env.KOTLIN_HOME}/lib/kotlin-ant.jar"/>
	<target name="-post-compile">
	<path id="project.javac.classpath">
	<path refid="project.all.jars.path" />
	<path refid="tested.project.classpath" />
	<path path="${java.compiler.classpath}" />
	<path path="${project.target.android.jar}"/>