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
"<w>" | |
"a" | |
"b" | |
"opt_a" | |
"opt_b" | |
"odd" | |
"even" | |
"^" | |
"$" | |
"<w>" |
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
BUILDFILE := ./buildfile.hs | |
BUILD := ./_build/build | |
BUILDDIR := $(dir $(BUILD)) | |
SOURCES := $(shell find .) | |
SOURCES := $(filter-out ./Makefile,$(SOURCES)) | |
SOURCES := $(filter-out $(BUILD),$(SOURCES)) | |
SOURCES := $(filter-out $(BUILDFILE),$(SOURCES)) | |
# Delegate the default task. | |
default: |
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 TemplateHaskell, QuasiQuotes, FlexibleInstances, FlexibleContexts, | |
TypeFamilies, GADTs, TypeOperators, DataKinds, PolyKinds, RankNTypes, | |
KindSignatures, UndecidableInstances, StandaloneDeriving, | |
RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-} | |
module AB where | |
import Prelude hiding (lookup, lex) | |
import Control.Applicative ((<|>),empty) | |
import Data.Maybe (maybeToList) |
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 agda2_compute_toplevel where | |
import Control.Concurrent (forkIO) | |
import Data.List (isPrefixOf) | |
import System.Environment (getEnv) | |
import System.FilePath (splitSearchPath) | |
import System.IO | |
import System.Process | |
import Text.Printf (printf) |
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 file contains the code from the paper "Formalising | |
-- type-logical grammars in Agda", and was directly extracted from the | |
-- paper's source. | |
-- | |
-- Note: because the symbol customarily used for the "left difference" | |
-- is unavailable in the Unicode character set, and the backslash used | |
-- for implication is often a reserved symbol, the source file uses a | |
-- different notation for the connectives: the left and right | |
-- implications are represented by the double arrows "⇐" and "⇒", and |
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 OverloadedStrings, RecordWildCards, TupleSections, DeriveFunctor #-} | |
> module Unlit where | |
> import Control.Arrow (first,second) | |
> import Data.List (foldl') | |
> import Data.Text (Text) | |
> import qualified Data.Text as T | |
> import qualified Data.Text.IO as T |
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
DROPBOX_SIZE_LIMIT=3000 | |
DROPBOX_FOLDER="$HOME/Dropbox" | |
DROPBOX_SHARED_INDEX="$DROPBOX_FOLDER/Shared/.index" | |
function share { | |
current=`du -s $DROPBOX_FOLDER | cut -f1` | |
# with no arguments, echo current usage | |
if [ "$#" -eq 0 ]; then |
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 DeriveDataTypeable #-} | |
import Control.Applicative ((<$>)) | |
import Control.Monad (filterM) | |
import Data.Foldable (or) | |
import Data.List (isSuffixOf,maximumBy) | |
import Data.Ord (comparing) | |
import Data.Traversable (traverse) | |
import Development.Shake | |
import Development.Shake.FilePath |
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
#!/usr/bin/env runhaskell | |
-- cabal depedencies: | |
-- | |
-- * containers | |
-- * pandoc-types | |
-- * uu-parsinglib | |
-- | |
{-# LANGUAGE RankNTypes #-} |
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 GADTs #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE UndecidableInstances #-} |