Sean Leather spl

## keybase.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                spl
                / keybase.md
            
            
              Created
              October 15, 2014 14:11
            
              
                keybase.md
              
          
    Keybase proof

I hereby claim:

I am spl on github.
I am seanleather (https://keybase.io/seanleather) on keybase.
I have a public key whose fingerprint is FBC2 C295 60BE A74A D943  B84A 8841 5DD3 E6DE AB1D

To claim this, I am signing this object:

  
## ToBoundedIntegral.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE MagicHash #-}

#include "MachDeps.h"

import GHC.Base
import GHC.Int
import GHC.Word
import Foreign.C.Types

## EitherFail.hs
$ ghci
GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help

-- This is a similar to a function found in some library somewhere.
Prelude> let lookupM k v = maybe (fail $ show k ++ " not found in " ++ show v) return $ lookup k v
Prelude> :t lookupM
lookupM
  :: (Eq a1, Monad m, Show a, Show a1) => a1 -> [(a1, a)] -> m a

-- What happens when you use Either as the monad?

## copy.hs
{-# OPTIONS_GHC -Wall #-}
module Main where
import Development.Shake

main :: IO ()
main = shakeArgs shakeOptions $ do
  want ["output-file"]
  "output-file" *> \dst ->
    copyFile' "input-file" dst

## copyWithDependency.hs
{-# OPTIONS_GHC -Wall #-}
module Main where
import Development.Shake

main :: IO ()
main = shakeArgs shakeOptions $ do
  want ["output-file"]
  "output-file" *> \dst -> do
    need ["dependency-file"]
    copyFile' "input-file" dst

## Main.hs
module Main where

import System.Console.Haskeline
import System.Environment
import Control.Exception (AsyncException(..))

{--
Testing the line-input functions and their interaction with ctrl-c signals.

Usage:

## ovpn-writer.sh
#!/bin/sh

##
## Usage: ./ovpn-writer.sh SERVER CA_CERT CLIENT_CERT CLIENT_KEY SHARED_SECRET > client.ovpn
##

server=${1?"The server address is required"}
cacert=${2?"The path to the ca certificate file is required"}
client_cert=${3?"The path to the client certificate file is required"}
client_key=${4?"The path to the client private key file is required"}

## instance_comparison.lean
/-
First, we add the necessary preliminary declarations:
-/

import data.list
open list

variable {A : Type}

/-

## .project
+ *.lean
- flycheck*.lean
- .#*.lean

## math.vim
" Originally from Dan Piponi
:map! \lolly ⊸
:map! \comp ∁
:map! \turn& ⅋
:map! \lneg ⅂
:map! \union ∪
:map! \cup ∪
:map! \cap ∩
:map! \alpha α
:map! \alpha α
	{-# LANGUAGE CPP #-}
	{-# LANGUAGE MagicHash #-}

	#include "MachDeps.h"

	import GHC.Base
	import GHC.Int
	import GHC.Word
	import Foreign.C.Types
	$ ghci
	GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help

	-- This is a similar to a function found in some library somewhere.
	Prelude> let lookupM k v = maybe (fail $ show k ++ " not found in " ++ show v) return $ lookup k v
	Prelude> :t lookupM
	lookupM
	:: (Eq a1, Monad m, Show a, Show a1) => a1 -> [(a1, a)] -> m a

	-- What happens when you use Either as the monad?
	{-# OPTIONS_GHC -Wall #-}
	module Main where
	import Development.Shake

	main :: IO ()
	main = shakeArgs shakeOptions $ do
	want ["output-file"]
	"output-file" *> \dst ->
	copyFile' "input-file" dst
	module Main where

	import System.Console.Haskeline
	import System.Environment
	import Control.Exception (AsyncException(..))

	{--
	Testing the line-input functions and their interaction with ctrl-c signals.

	Usage:
	#!/bin/sh

	##
	## Usage: ./ovpn-writer.sh SERVER CA_CERT CLIENT_CERT CLIENT_KEY SHARED_SECRET > client.ovpn
	##

	server=${1?"The server address is required"}
	cacert=${2?"The path to the ca certificate file is required"}
	client_cert=${3?"The path to the client certificate file is required"}
	client_key=${4?"The path to the client private key file is required"}
	/-
	First, we add the necessary preliminary declarations:
	-/

	import data.list
	open list

	variable {A : Type}

	/-
	" Originally from Dan Piponi
	:map! \lolly ⊸
	:map! \comp ∁
	:map! \turn& ⅋
	:map! \lneg ⅂
	:map! \union ∪
	:map! \cup ∪
	:map! \cap ∩
	:map! \alpha α
	:map! \alpha α