Larry Diehl larrytheliquid

Actors

The Ultimate Git Alias Setup

If you use git on the command-line, you'll eventually find yourself wanting aliases for your most commonly-used commands. It's incredibly useful to be able to explore your repos with only a few keystrokes that eventually get hardcoded into muscle memory.

Some people don't add aliases because they don't want to have to adjust to not having them on a remote server. Personally, I find that having aliases doesn't mean I that forget the underlying commands, and aliases provide such a massive improvement to my workflow that it would be crazy not to have them.

The simplest way to add an alias for a specific git command is to use a standard bash alias.

# .bashrc

	Mathematical Logic - Kleene
	Basic Category Theory for Computer Scientists - Pierce
	A Book of Abstract Algebra - Pinter
	Conceptual Mathematics - Lawvere & Schanuel
	An Introduction to Formal Logic - Smith
	To Mock A Mockingbird - Smullyan
	Introduction To Logic - Tarski
	Purely Functional Data Structures - Okasaki
	Topoi: The Categorial Analysis of Logic - Goldblatt
	Lectures on the Curry-Howard Isomorphism - Sorensen, Urzyczyn

	module Maths where

	data Nat : Set where
	zero : Nat
	suc : Nat → Nat

	plus : Nat → Nat → Nat
	plus zero n = n
	plus (suc m) n = suc (plus m n)

	-- This is going to be on Hackage soon! https://github.com/gatlin/surely

	{-# LANGUAGE BangPatterns #-}

	-- \|
	-- Module : AI.Surely
	-- Copyright : 2012 Gatlin Johnson
	-- License : LGPL 3.0
	-- Maintainer : [email protected]
	-- Stability : experimental

	module Routing where

	open import Function hiding (type-signature)

	open import Data.Bool hiding (_≟_)
	open import Data.Maybe
	open import Data.Char hiding (_≟_)
	open import Data.String as String
	open import Data.List as List hiding ([_])
	open import Data.Product hiding (curry; uncurry)

	module Categories.Agda.State where

	open import Categories.Category
	open import Categories.Agda
	open import Categories.Agda.Product
	open import Categories.Functor hiding (_≡_)
	open import Categories.Functor.Product
	open import Categories.Functor.Hom
	open import Categories.Monad
	open import Categories.Adjunction

	open import Data.Empty using ( ⊥ ; ⊥-elim )
	open import Data.Unit using ( ⊤ ; tt )
	open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
	renaming ( _≟_ to _≟B_ )
	open import Data.Nat using ( ℕ ; zero ; suc )
	renaming ( _≟_ to _≟ℕ_ )
	open import Data.Product using ( Σ ; _,_ )
	open import Relation.Nullary using ( Dec ; yes ; no )
	open import Relation.Binary using ( Decidable )
	open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

	{-
	How does local completeness (http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf) generalize to eliminators?

	Below is the eliminator for `ℕ` that does not include the inductive hypothesis `P n` in the `suc n` branch.
	It still passes local completeness because the `suc n` branch still includes the `n` index, it merely omits the inductive hypothesis.

	Caveats:
	1. `ℕ` is a datatype rather than a standard logical proposition, and it has many proofs/inhabitants for the same type.
	2. I'm being more strict here by requiring the expansion to equal the input, rather than merely proving the same proposition.
	-}

	{-# LANGUAGE DeriveDataTypeable , Rank2Types , ViewPatterns #-}
	import Control.Applicative
	import Control.Arrow
	import Control.Monad.Reader
	import Control.Monad.Writer
	import Data.Generics
	import Data.Set (Set)
	import qualified Data.Set

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