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 --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 |
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
# 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 |
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
%====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 |
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
#!/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…" |
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
#!/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 |
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 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 |
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 #-} | |
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 |
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 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_; _⇒_) |
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 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 |
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
// 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" |
NewerOlder