treeowl

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs,
      ScopedTypeVariables, TypeOperators #-}

-- | Type-level natural numbers and singletons, with proofs of
-- a few basic properties.

module BasicNat (
    -- | Type-level natural numbers
    Nat (..)
  , type (+)

ymjing

Powerline-patched Monaco for Windows and OSX

This font is manually patched with Fontforge. It includes the glyphs from DejaVu Sans Mono for Powerline.

I recommend DirectWrite-patched VIM builds. I'm using KaoriYa's build (http://www.kaoriya.net/software/vim/)

Usage

Add the following lines to your .vimrc/_vimrc:

twanvl

-- Formalization of untyped lambda calculus
module 2013-10-23-lambda where

open import Level hiding (zero;suc)
open import Function using (_∘_;id;_⟨_⟩_)
open import Data.Empty
open import Data.Star as Star using (Star;_◅_;_◅◅_;ε;_⋆)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Data.Product as P hiding (map;zip)

itspriddle

http://hea-www.harvard.edu/~fine/OSX/unicode_apple_logo.html

•  -  -  - the Apple Symbol
• ⌘ - ⌘ - ⌘ - the Command Key symbol
• ⌥ - ⌥ - ⌥ - the Option Key symbol
• ⇧ - ⇧ - ⇧ - the Shift Key symbol
• ⎋ - ⎋ - ⎋ - the Escape Key symbol

And while we're at it, some related (not mac-specific):