JasonGross

import Init.Meta

-- This isn't strictly necessary of course - reverse could be a member of `Range`.
class Reverse (α : Type u) where
  reverse : α → α 

open Reverse (reverse)


-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --

JasonGross

import tactic.norm_num
import algebra.group_power
open prod
universes u v w ℓ

inductive let_bound (α : Type*)
| base : α → let_bound
| dlet : ℤ → (ℤ → let_bound) → let_bound
| mlet {β : Type} : β → (β → let_bound) → let_bound
open let_bound

JasonGross

#!/usr/bin/env bash
# memusg -- Measure memory usage of processes
# Usage: memusg COMMAND [ARGS]...
#
# Author: Jaeho Shin <netj@sparcs.org>
# Created: 2010-08-16
set -um

# check input
[ $# -gt 0 ] || { sed -n '2,/^#$/ s/^# //p' <"$0"; exit 1; }

JasonGross

(** A 0-skeletal filling of an l-simplex is (S l) vertices.
    A (S k)-skeletal filling of an l-simplex has (S l) C (S k)  (S k)-cells
    matching their boundaries in a k-skeletal filling of an l-simplex;
    where to say the (S k)-cell matches its boundary is to say that its boundary
    is the underlying k-skeletal filling of its underlying (S k)-simplex.
 *)

(** This is both the heart of the matter, and the weakest link; for some reason
    this presentation of n C k makes it very difficult to prove equations.
    Perhaps some clever person can rework the whole around a different presentation.