rplacd

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.

rplacd

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

rplacd

# COMMENTARY ON RETRO68 APPLICATION BUILD PROCESS
# ===============================================
#
# About
# =====
# Retro68, the cross-compiler toolchain for the classic 68k Macintosh (e.g. System 7), uses
# cmake makefiles. I prefer to use standard makefiles. To reverse-engineer how Retro68
# builds a sample application with a custom resource file, I built the sample application
# Samples/Dialog.
#