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.

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

[apply]
  whitespace = nowarn

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

[alias]
  a = "add"

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

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

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

#!/bin/sh

# This script will setup Evm (Emacs Version Manager) and Cask on
# Travis to use for Emacs Lisp testing.
#
# In .travis.yml, add this:
#
#  - curl -fsSkL https://gist.github.com/rejeep/7736123/raw > travis.sh && source ./travis.sh
#
# Emacs 24.3 is installed in the above script because Cask requires

soonhokong

#!/bin/sh

# This script will setup Evm (Emacs Version Manager) and Cask on
# Travis to use for Emacs Lisp testing.
#
# In .travis.yml, add this:
#
#  - curl -fsSkL https://gist.github.com/rejeep/7736123/raw > travis.sh && source ./travis.sh
#
# Emacs 24.3 is installed in the above script because Cask requires

soonhokong

#! /usr/bin/env bash

# Author: Damien Cassou
#
# This is the script I use to build Emacs packages for Ubuntu. These
# packages are uploaded to
# https://launchpad.net/~cassou/+archive/emacs/. Each package is
# either build from a Debian package or from
# http://emacs.naquadah.org/.

soonhokong

Code from CAPD Author

#include <iostream>
#include "capd/capdlib.h"
using namespace std;
using namespace capd;

int main(){
  cout.precision(17);