larrytheliquid

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

larrytheliquid

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)

gatlin

-- 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       : rokenrol@gmail.com
-- Stability        : experimental

copumpkin

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)

copumpkin

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

larrytheliquid

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 )

larrytheliquid

{-
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.
-}

halorgium

Actors

• ATOM
• Celluloid
• Akka
  • Handbook
  • Inspirators
  • Book
• Erlang
• Thesis

ntc2

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

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

mwhite

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