Soonho Kong 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.

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

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

#!/usr/bin/env bash

[apply]
  whitespace = nowarn

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

[alias]
  a = "add"

Code from CAPD Author

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

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

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

	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

	-- 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) :=

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

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

	#! /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/.