ekmett

{-# Language CPP #-}
{-# Language BlockArguments #-}
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language ViewPatterns #-}
{-# Language TypeApplications #-}
{-# Language BangPatterns #-}
{-# Language TypeOperators #-}
{-# Language TypeFamilyDependencies #-}
{-# Language DataKinds #-}

marek-safar

static const AssemblyVersionMap framework_assemblies [] = {
	{"Accessibility", 0},
	{"Commons.Xml.Relaxng", 0},
	{"I18N", 0},
	{"I18N.CJK", 0},
	{"I18N.MidEast", 0},
	{"I18N.Other", 0},
	{"I18N.Rare", 0},
	{"I18N.West", 0},
	{"Microsoft.Build.Engine", 2, NULL, TRUE},

marcan

#!/boot/bzImage

# Linux kernel userspace initialization code, translated to bash
# (Minus floppy disk handling, because seriously, it's 2017.)
# Not 100% accurate, but gives you a good idea of how kernel init works
# GPLv2, Copyright 2017 Hector Martin <[email protected]>
# Based on Linux 4.10-rc2.

# Note: pretend chroot is a builtin and affects the current process
# Note: kernel actually uses major/minor device numbers instead of device name

tel

/// PRELIMINARIES

/**
 * Generalized "products" of any size. For gluing things together. A tuple is a
 * "2"-meet.
 *
 * The type `Meet a b c d ...` indicates a `Meet` of the given size with values
 * at each type in the sequence.
 */

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE LambdaCase #-}

-- Code obviously based on <http://andrej.com/plzoo/html/levy.html>

-- This is right now *not really* CBPV. In particular, the Rec binder
-- is both less well-behaved and far more complex than it ought to
-- be. Instead of passing a computation back (which should never be
-- possible as variables do not have computation types) it should pass
-- back a thunk.

gallais

module reornament where

open import Data.Product
open import Data.Nat
open import Data.List

ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)

data ListSpec (A : Set) {B : Set} (alg : ListAlg A B) : (b : B) → Set where

mzero

#!/bin/sh

inPreprocessorMode () {
    hasE=0
    hasU=0
    hasT=0
    for arg in "$@"
    do
        if [ 'x-E' = "x$arg" ];             then hasE=1; fi
        if [ 'x-undef' = "x$arg" ];         then hasU=1; fi

copumpkin

module Unify where

-- Translated from http://strictlypositive.org/unify.ps.gz

open import Data.Empty
import Data.Maybe as Maybe
open Maybe hiding (map)
open import Data.Nat
open import Data.Fin
open import Data.Product hiding (map)

davetron5000

davetron5000's ideal presentation software

• Editable as text, preferably markdown
• Plays in a browser
• Deployable to heroku or other service completely statically
• clean default look that is easy to customize without slogging through generated HTML
• hard-fix the dimensions, e.g. 1024x768 for projectors
• support for remote control for advancing

Slide Types

takumikinjo

README.html