jrudolph

/*
 * This is the Towers of Hanoi example from the prolog tutorial [1]
 * converted into Scala, using implicits to unfold the algorithm at
 * compile-time. 
 * 
 * [1] http://www.csupomona.edu/~jrfisher/www/prolog_tutorial/2_3.html
 */

object TowersOfHanoi {
  import scala.reflect.Manifest

karmi

.DS_Store
*.log
tmp/

jsuereth

package scalaz.example.nio

import scalaz._
import concurrent.Promise
import effects.IO
import nio.sockets._
import nio.Channels._
import Scalaz._
import iteratees._
import java.nio.channels.SocketChannel

gist:1196136

{- # OPTIONS_GHC -fglasgow-exts    #-} -- For deriving Data/Typeable
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards, TypeSynonymInstances, DeriveDataTypeable #-}

import IO
import Control.Monad
import Control.OldException(catchDyn,try)
import XMonad.Util.Run
import Control.Concurrent
import DBus
import DBus.Connection

bitonic

{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}
-- Laungh ghci with -fobject-code to make the Fix/Tree trick work (thanks edwardk).

-- courtesy of hpc on #haskell
import Unsafe.Coerce
import Control.Monad.ST

toInteger :: Int -> Integer
isJust :: Maybe a -> Bool
null :: [a] -> Bool

copumpkin

module Nicomachus where

open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning

open import Data.Nat
open import Data.Nat.Properties

-- http://en.wikipedia.org/wiki/Nicomachus%27s_theorem

acowley

(* Ported from Dan Peebles's proof at: https://gist.github.com/2356060 *)
Module SquaredTriangular.
Require Import Arith.

Definition N := nat.

(* Sigma notation for expressing sums. *)
Fixpoint Σ (x : N) (f : N -> N) : N :=
  match x with
  | 0 => 0

max-mapper

Government OAuth

OAuth is a popular technology that companies like Facebook and Twitter have used to integrate with applications developed by outside parties (e.g. "Sign in with Twitter")

Goals:

• "Sign in with your City of XYZ account" on community/third party developed web apps
• per-transaction/fixed rate/etc payments from gov to NGO developers
• lightweight tech procurement via API (as opposed to the system currently in place: see http://requestforawesome.com)
• ability to start and cancel contracts eeasily -- think Heroku Add-ons for government services

tomprince

    (eval-after-load 'agda2-mode
      '(progn
         (evil-define-key 'normal agda2-mode-map
           "\\a" 'agda2-auto
           "\\k" 'agda2-previous-goal
           "\\j" 'agda2-next-goal
           "\\c" 'agda2-make-case
           "\\d" 'agda2-infer-type-maybe-toplevel
           "\\e" 'agda2-show-context
           "\\l" 'agda2-load

mads-hartmann

object Peano {
  
  sealed trait Nat
  trait Zero extends Nat
  object ZeroV extends Zero
  case class Succ[A <: Nat](x: A) extends Nat

  trait Sum[A <: Nat, B <: Nat] {
    type Out <: Nat
  }