Lîm Tsú-thuàn dannypsnl

Grope

A grope is a set $G$ together with a binary operation $\circ$, in which the identity

$$ x \circ (y \circ x) = y $$

is satisfied for all $x, y \in G$.

	{-
	This file demonstrates a technique for making working with de Bruijn-indexed
	terms easier that I learnt from the paper /The Linearity Monad/ by Jennifer
	Paykin and Steve Zdancewic. After defining well-typed terms `Γ ⊢ τ` using de Bruijn
	indices, we define an auxiliary function `lam` that takes in the variable term explicitly:

	> lam : {V : Type} {Γ : Cxt V} {τ σ : Ty V}
	> → (({Δ : Cxt V} → {{IsExt Δ (Γ , τ)}} → Δ ⊢ τ)
	> → (Γ , τ) ⊢ σ)
	> → Γ ⊢ τ ⇒ σ

	#lang racket
	(require (for-syntax syntax/parse))

	(define (reify-name n)
	(string->symbol
	(string-append "_" (number->string n))))
	(struct fresh (value count)
	#:methods gen:custom-write
	[(define (write-proc self out mode)
	(if (fresh-value self)

	#lang racket
	(require (for-syntax syntax/parse))

	(define-syntax (math stx)
	(syntax-parse stx
	#:datum-literals (+ *)
	[(_ (o ...) op o* ...)
	#'(let ([k (math o ...)])
	(math k op o* ...))]
	[(_ (o ...)) #'(math o ...)]

	#lang racket
	(require pict
	rebellion/collection/multiset)

	(define (square bit)
	(define pict-size 5)
	(match bit
	[1 (filled-rectangle pict-size pict-size)]
	[0 (rectangle pict-size pict-size)]))