This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --copatterns #-} | |
module CoList where | |
{- High-level intuition: | |
codata CoList (A : Set) : Set where | |
nil : CoList A | |
cons : A → CoList A → CoList A | |
append : ∀{A} → CoList A → CoList A → CoList A |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE FlexibleContexts #-} | |
module PickRandom where | |
import Data.List (group, sort) | |
import Control.Monad | |
import Control.Monad.Random (MonadRandom, getRandomR) | |
import qualified Control.Foldl as F | |
-- Pick a value uniformly from a fold | |
pickRandom :: MonadRandom m => a -> F.FoldM m a a | |
pickRandom a = F.FoldM choose (return (a, 0 :: Int)) (return . fst) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Problem 3 of @Hillelogram's Great Theorem Prover Showdown. | |
-- https://www.hillelwayne.com/post/theorem-prover-showdown | |
-- | |
-- Implemented using current stable-2.5 branch of Agda | |
-- (https://github.com/agda/agda/tree/08664ac) and the agda-prelude | |
-- library (https://github.com/UlfNorell/agda-prelude/tree/d193a94). | |
module Fulcrum where | |
open import Prelude hiding (_≤?_) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
%default total | |
data Format | |
= FInt -- %d | |
| FString -- %s | |
| FOther Char -- [a-zA-Z0-9] | |
format : List Char -> List Format |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module RuntimeTypes where | |
open import Function | |
open import Data.Unit | |
open import Data.Bool | |
open import Data.Integer | |
open import Data.String as String | |
open import Data.Maybe hiding (All) | |
open import Data.List | |
open import Data.List.All |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
project=$(basename "$(pwd)") | |
# build dependencies | |
build_deps="stack build $project --fast --pedantic --dependencies-only --interleaved-output" | |
# restart on changes in other packages | |
restarts=$(find ../. -maxdepth 1 -type d \ | |
-not -name "$project" \ | |
-not -name .stack-work \ | |
-not -name . \ |
Various blog posts related to Nix and NixOS
- https://nixos.org/wiki/Main_Page Nix wiki. Awesome resource containing huge amount of manuals and documentation with examples.
- http://aflatter.de/nixos/ Alexander Flatter - NixOS. Installing NixOS inside a VirtualBox with a real-world
configuration.nix
example. - http://lethalman.blogspot.it/search/label/nixpills Luca Bruno - Nix Pills. Series of posts describing how to install nix into some environment and how to use it.
- http://looprecur.com/blog/from-ubuntu-to-nixos/ Tim Sears - From Ubuntu to NixOS. Talk about experience migrating from Ubuntu to NixOS.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Haskell Mergesort | |
- Copyright (C) 2014 by Kendall Stewart | |
First we define a couple of helper functions that | |
will be useful in splitting the list in half: | |
> fsthalf :: [a] -> [a] | |
> fsthalf xs = take (length xs `div` 2) xs |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- This is going to be on Hackage soon! https://github.com/gatlin/surely | |
{-# LANGUAGE BangPatterns #-} | |
-- | | |
-- Module : AI.Surely | |
-- Copyright : 2012 Gatlin Johnson | |
-- License : LGPL 3.0 | |
-- Maintainer : rokenrol@gmail.com | |
-- Stability : experimental |