Richard Mongler rplacd

## real_time_integer_dithering.html
<!-- We Timothy Robards' webcam filter codepen as a starting
    point for this webcam B or W conversion test.
    https://codepen.io/trobes/pen/bxropm
-->

<!--
    PURPOSE: this is a Canvas-based prototype of a RGB-to-grayscale-to-dithered BandW
    conversion scheme that
    – can be done, per pixel, immediately after generating a source pixel colour;
    – uses storage at most equal to one graphics buffer, plus a comparatively small

## NaturalDeduction_and_SequentCalculus.v
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.

(** * A taste of Curry-Howard

In particular, how do we show a λ-calculus term is valid proof for a logical proposition?

** An overview

To be more specific: I assume you've worked before with deduction systems that are given in the assumptions-over-conclusion notation. (If you've seen them stacked on top of each other in proof trees, so much the better.) In particular, if you understand a definition in that form of a relation like the has-type or evaluates-to relation, you should be set.

## NaturalDeduction_and_SequentCalculus.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<style type="text/css">
body { padding: 0px 0px;
       margin: 0px 0px;
       background-color: white }

## tumblr-downloader.js
"use strict";

/*
  tumblr-downloader.js - a Node.js script to download all media files posted in
  a Tumblr blog, most recent first.

  Usage:
    node tumblr-downloader.js

    Options - domain to download from, API key, and so on - are exposed below.

## Bookbinding.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                rplacd
                / Bookbinding.md
            
            
              Last active
              July 27, 2016 20:21
            
              
                Paperbacks with a laser printer, effort, and trial and error.
              
          
    Bookbinding, with a few gotchas covered


or: How I printed and bound a 600 page book in less than one day
Dylan McNamee

This guide is a result of following Dylan McNamee’s own: it adds in missing details (stack trimming included), and covers a few hiccups to avoid. What is here wouldn’t have been possible without his guide.
What’s covered, and what isn’t

  
## CoqIDE bundled with ssreflect.md

      
              1 file
            
          
              1 fork
            
          
              0 comments
            
          
              0 stars
            
          
                rplacd
                / CoqIDE bundled with ssreflect.md
            
            
              Last active
              June 10, 2017 23:34
            
              
                CoqIDE (8.5pl1, OS X) bundled with ssreflect.
              
          
    The CoqIDE bundle (8.5pl1, OS X) with ssreflect preinstalled.

coqide-8.5pl1-ssreflect.7z - around 75 MB. (Smaller than the standard CoqIDE bundle!)
A great big caveat: the app bundle is no longer codesigned. If you wish to keep CoqIDE*.app codesigned, install a clean CoqIDE*.app, and replace the Resource/bin and Resources/lib/coq/user-contrib with the ones here.
Sanity testing the installation

I’m sure the reference manual is out of date - instead, I use test cases from the mathcomp/ssrtest folder. Note the new, extended library import paths. Try this, for example:

  
## LamPi.lidr
> module Micro
> import Data.String

Another implementation of λ_Π
=============================

An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if
- you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it;
- you can write a Scheme metacircular interpreter;
- understand how to write the usual suspects in an expressive type system like Idris';

## lxx2md.hs
#!/usr/bin/env stack
-- stack runghc --package text --package turtle

{-# LANGUAGE OverloadedStrings #-}

{-
  lxx2md.hs (-l|--lang LANG)
  A filter that converts Bird-style lhs in Markdown ``` blocks.
  Combines consecutive Bird-tracked lines into single blocks.

## LamPi.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                rplacd
                / LamPi.md
            
            
              Last active
              May 11, 2016 18:42
            
              
                Another implementation of λ_Π.
              
          
     module Micro
 import Data.String
Another implementation of λ_Π

An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if

you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it;


## gist:0e41a887aa85b414353a
By “world generation” we mean natural landscapes - not because we’re not interested in urban landscapes, but because we have a larger margin of error with the former. It’s not the “cities aren’t actually that interesting” effect - isn’t raw nature just as repeating? It’s the problem of simulating, in a way that isn’t trivial, all the possible ways humanity can both inhabit an environment, and shape it to its structures - determinism in both directions.

A high-level view. We’ll use Dwarf Fortress, Minecraft, Sir, You are Being Hunted, and The Witcher 3 (that is, the REDengine 3) as our prototypical examples. Be familiar with the first two. (TW3 isn’t meaningfully procedural - but substantially procedural enough to work on, and high-detail.)

We also refer to Morrowind as a source world we intend to model.

We begin with concrete analyses, work out the design space, and then try to locate ourselves within it - although you can read it backwards if you want to see choices before justifications.

A concrete exam
	<!-- We Timothy Robards' webcam filter codepen as a starting
	point for this webcam B or W conversion test.
	https://codepen.io/trobes/pen/bxropm
	-->

	<!--
	PURPOSE: this is a Canvas-based prototype of a RGB-to-grayscale-to-dithered BandW
	conversion scheme that
	– can be done, per pixel, immediately after generating a source pixel colour;
	– uses storage at most equal to one graphics buffer, plus a comparatively small
	Require Import Coq.Strings.String.
	Require Import Coq.Lists.List.

	(** * A taste of Curry-Howard

	In particular, how do we show a λ-calculus term is valid proof for a logical proposition?

	** An overview

	To be more specific: I assume you've worked before with deduction systems that are given in the assumptions-over-conclusion notation. (If you've seen them stacked on top of each other in proof trees, so much the better.) In particular, if you understand a definition in that form of a relation like the has-type or evaluates-to relation, you should be set.
	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
	"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
	<html xmlns="http://www.w3.org/1999/xhtml">
	<head>
	<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
	<style type="text/css">
	body { padding: 0px 0px;
	margin: 0px 0px;
	background-color: white }
	"use strict";

	/*
	tumblr-downloader.js - a Node.js script to download all media files posted in
	a Tumblr blog, most recent first.

	Usage:
	node tumblr-downloader.js

	Options - domain to download from, API key, and so on - are exposed below.
	> module Micro
	> import Data.String

	Another implementation of λ_Π
	=============================

	An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if
	- you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it;
	- you can write a Scheme metacircular interpreter;
	- understand how to write the usual suspects in an expressive type system like Idris';
	#!/usr/bin/env stack
	-- stack runghc --package text --package turtle

	{-# LANGUAGE OverloadedStrings #-}

	{-
	lxx2md.hs (-l\|--lang LANG)
	A filter that converts Bird-style lhs in Markdown ``` blocks.
	Combines consecutive Bird-tracked lines into single blocks.
	By “world generation” we mean natural landscapes - not because we’re not interested in urban landscapes, but because we have a larger margin of error with the former. It’s not the “cities aren’t actually that interesting” effect - isn’t raw nature just as repeating? It’s the problem of simulating, in a way that isn’t trivial, all the possible ways humanity can both inhabit an environment, and shape it to its structures - determinism in both directions.

	A high-level view. We’ll use Dwarf Fortress, Minecraft, Sir, You are Being Hunted, and The Witcher 3 (that is, the REDengine 3) as our prototypical examples. Be familiar with the first two. (TW3 isn’t meaningfully procedural - but substantially procedural enough to work on, and high-detail.)

	We also refer to Morrowind as a source world we intend to model.

	We begin with concrete analyses, work out the design space, and then try to locate ourselves within it - although you can read it backwards if you want to see choices before justifications.

	A concrete exam