marklemay

# https://en.wikipedia.org/wiki/Three-card_Monte


def shuffle(i, cards):
    """ shuffles a list of cards for i iterations """
    tmp = cards
    cards[0] = cards[1]
    cards[1] = cards[2]
    cards[2] = tmp[0]
    if i > 0:

marklemay

# see http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/


def cons(head, tail):
    def out(i):
        if i == 0:
            return head
        else:
            return tail(i - 1)

marklemay

{-# OPTIONS --type-in-type #-}
-- TODO: turn this off and see what happens!

-- Burali-Forti's paradox in MLTT-ish without W-types

-- I was following Coquand's paper "An Analysis of Girard's Paradox"
-- and Hurkens's paper "A Simplification of Girard's Paradox".
-- Code is released under CC0.

module BuraliFortiParadox where

marklemay

(* -*- mode: ocaml; -*- *)

module type FUNCTOR = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}

type var = string

marklemay

I just had to set up Jenkins to use GitHub. My notes (to myself, mostly):

Detailed Instructions

For setting up Jenkins to build GitHub projects. This assumes some ability to manage Jenkins, use the command line, set up a utility LDAP account, etc. Please share or improve this Gist as needed.

Install Jenkins Plugins

• get both the git and github plugin
• http://wiki.jenkins-ci.org/display/JENKINS/Git+Plugin

marklemay

module TicTacToe where

open import Data.Bool
  using (Bool; true; false; _∧_; _∨_)
open import Data.Empty
  using (⊥-elim)
open import Data.Fin
  using (Fin; zero; suc)
open import Data.Maybe
  using (Maybe; just; nothing)