cartazio

{-# OPTIONS --type-in-type #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product

data Ty : Set where
  U : Ty
  Pi : (A : Set) -> (A -> Ty) -> Ty
  PiInd : Ty -> Ty

cartazio

# You don't need Fog in Ruby or some other library to upload to S3 -- shell works perfectly fine
# This is how I upload my new Sol Trader builds (http://soltrader.net)
# Based on a modified script from here: http://tmont.com/blargh/2014/1/uploading-to-s3-in-bash

S3KEY="my aws key"
S3SECRET="my aws secret" # pass these in

function putS3
{
  path=$1

cartazio

%====Set up Listings===============================================================

\definecolor{darkgreen}{rgb}{0,0.5,0}
\definecolor{darkred}{rgb}{0.5,0,0}
\lstloadlanguages{Haskell}
\lstnewenvironment{code}
    { % \centering
      \lstset{}%
      \csname lst@SetFirstLabel\endcsname}
    { %\centering

cartazio

#!/bin/bash
cabal configure && cabal build && cabal haddock --hyperlink-source
S=$?
if [ "${S}" -eq "0" ]; then
    cd "dist/doc/html"
    DDIR="${1}-${2}-docs"
    cp -r "${1}" "${DDIR}" && tar -c -v -z -Hustar -f "${DDIR}.tar.gz" "${DDIR}"
    CS=$?
    if [ "${CS}" -eq "0" ]; then
        echo "Uploading to Hackage…"

cartazio

#!/bin/bash

# Options / Usage
# put this script in the same directory as your *.cabal file
# it will use the first line of "cabal info ." to determine the package name

# custom options for "cabal install"
CUSTOM_OPTIONS=(--haddock-options='-q aliased')
# hackage server to upload to (and to search uploaded versions for)
HACKAGESERVER=hackage.haskell.org

cartazio

{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies, TypeOperators,
             ConstraintKinds, ScopedTypeVariables, RankNTypes #-}

module Shape where

import GHC.Exts
import Data.Proxy
import Data.Type.Equality

data Nat = Zero | Succ Nat

cartazio

{-# LANGUAGE OverloadedStrings #-}

module Git where

import           Data.Text.Lazy      (Text)
import qualified Data.Text.Lazy      as T
import           Prelude             hiding (FilePath)
import           Shelly

git :: [Text] -> Sh Text

cartazio

module Weird where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Product
open import Data.Conat
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary using (module Setoid; _Respects_; _⇒_)

cartazio

{-# Language ExistentialQuantification, GADTs #-}

module Control.Process where

import Data.Monoid
import Prelude hiding (zip, zipWith)
import Control.Applicative
import System.IO

data Process f a = Halt 

cartazio

// Originally based on PyAliasAnalysis from the unladen-swallow project!
#include "llvm/ADT/APInt.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/SmallPtrSet.h"
#include "llvm/Analysis/AliasAnalysis.h"
#include "llvm/Analysis/ScalarEvolution.h"
#include "llvm/Analysis/ScalarEvolutionExpressions.h"
#include "llvm/Analysis/Passes.h"
#include "llvm/Argument.h"
#include "llvm/Constants.h"