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)