petermarks

record R where
 constructor MkR
 foo : Nat

foo_identity : (foo (set_foo x r)) = x
foo_identity {x} {r} with (foo (set_foo x r))
  foo_identity {x} | y = ?rhs

petermarks

 #{ stdenv, fetchurl, qtbase, qtmultimedia, qttools, alsa-lib, libusb }: 
 with import <nixpkgs> {};

# TODO: disable some plugins

 stdenv.mkDerivation {
  name = "qlcplus-4.11.0";
  src = ./qlcplus-QLC-_4.11.0;
  buildInputs = [ qt5.qtbase qt5.qtscript qt5.qtmultimedia qt5.qttools alsaLib libusb libudev qt5.qmakeHook ];
  nativeBuildInputs = [ pkgconfig ];

petermarks

{ stdenv }:

stdenv.mkDerivation
	{ name = "website";
		src = ../code;
		phases = [ "installPhase" ];
		installPhase = ''
			mkdir -p $out
			cp -r * $out/
			ln -s /data/files $out

petermarks

module Alloc where

import Data.List
import Control.Arrow

data Allocs = Allocs {checkouts :: [Int], checkins :: [Int]} deriving (Eq, Show)


allocs :: [[Int]] -> (Int, [Allocs])
allocs = first length . mapAccumL f []

petermarks

module Bot where

import Control.Monad.Reader
import Control.Monad.Cont
import Data.List

data Command 
  = NoAction
  | Fire
  | Accelerate

petermarks

{-# language TypeSynonymInstances, FlexibleInstances, DeriveDataTypeable #-}

module GPretty where

import Data.Data
import Data.Typeable
import Data.Generics.Aliases

data Tree a = Node a [Tree a]
			deriving (Show, Data, Typeable)

petermarks

{-# LANGUAGE ViewPatterns, GADTs, KindSignatures, ScopedTypeVariables #-}
import Data.List

foldr2 :: (a -> b -> b) -> b -> [a] -> b
foldr2 f b [] = b
foldr2 f b (x:xs) = f x (foldr2 f b xs)

foldr3 :: ((a,b)->b,()->b) -> [a] -> b
foldr3 (f,b) [] = b ()
foldr3 (f,b) (x:xs) = f (x, foldr3 (f,b) xs)

petermarks

{-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses  #-}
module Puzzle where

import Data.List


--------------------------------------------------------------------------------
-- Specific to this puzzle

main :: IO ()

petermarks

module Main where

import Control.Monad
import Control.Monad.Logic
import Control.Monad.State.Strict
import qualified Data.Map as M

type BindingT k v = StateT (M.Map k v)

bind :: (Ord k, Eq v, Monad m) => k -> v -> BindingT k v m ()

petermarks

{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable #-}
module Coded where

import Control.Unification
import Control.Unification.IntVar
import Control.Monad.Logic
import Data.Functor.Fixedpoint
import Data.List
import Data.Foldable
import Data.Traversable