soonhokong

-- Theorems/Exercises from "Logical Investigations, with the Nuprl Proof Assistant"
-- by Robert L. Constable and Anne Trostle
-- http://www.nuprl.org/MathLibrary/LogicalInvestigations/
import logic

-- 2. The Minimal Implicational Calculus
theorem thm1 {A B : Prop} : A → B → A :=
assume Ha Hb, Ha

theorem thm2 {A B C : Prop} : (A → B) → (A → B → C) → (A → C) :=

soonhokong

import algebra.category.functor
open category eq eq.ops functor

inductive natural_transformation {C D : Category} (F G : C ⇒ D) : Type :=
mk : Π (η : Π(a : C), hom (F a) (G a)), (Π{a b : C} (f : hom a b), G f ∘ η a = η b ∘ F f)
 → natural_transformation F G

infixl `⟹`:25 := natural_transformation -- \==>

namespace natural_transformation

soonhokong

;; Package
(require 'package)
(add-to-list 'package-archives
             '("melpa" . "http://melpa.milkbox.net/packages/") t)
(package-initialize)
(package-refresh-contents)

;; Install required/optional packages for lean-mode
(defvar lean-mode-required-packages
  '(company dash dash-functional flycheck whitespace-cleanup-mode

soonhokong

[apply]
  whitespace = nowarn

[core]
        whitespace = trailing-space, space-before-tab
        autocrlf = input

[alias]
  a = "add"

soonhokong

takeshot.sh

We are using imagesnap program to take a photo from command-line. On OSX, you can install it via homebrew.

#!/usr/bin/env bash

soonhokong

Scenario

• We want to move all files under library/hott in leanprover/library repo to src/library/hott in leanprover/lean repo.
• We want to preserve the commit history of leanprover/library during the migration.

Solution

I assume that leanprover/lean repo is already cloned at ~/work/lean.