Skip to content

Instantly share code, notes, and snippets.

Carter Tazio Schonwald cartazio

Block or report user

Report or block cartazio

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View auth-toy.agda
module auth where
open import Data.String
open import Data.Nat
open import Level
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality as Het
View auth-toy.agda
module auth where
open import Data.String
open import Level
data AsDelegate : Set where
IsDelegate : AsDelegate
IsLeaf : AsDelegate
View gist:1abc5d5a85060fd71d33e60eb198a293
{
"add_to_PATH":
[
"/Users/carter/.cabal/bin",
"/Users/carter/.install-ghc/ghc-8.2.2/bin",
"/Users/carter/bin"
],
"auto_build_mode": "normal",
"auto_completion_popup": true,
"add_default_completions": true,
View BadUncurry.hs
module BadUncurry where
import Control.Exception
data Fst a = Only a deriving (Show, Typeable, Exception)
badFst :: (Typeable a, Show a) => a -> b -> c
badFst a = throw (Only a)
notOnly (Only a) = a
View gist:ad8cef5cf38a2bc4266b93d0c098902b
$ for i in (seq 255); sudo ifconfig lo0 alias 127.0.0.$i ; end
Password:
16:00:16 ~/W/p/a/W/c/numerical (master|✚7…) $ nc -l 0:0:0:0:0:ffff:7f00:50 80
nc: Permission denied
16:00:29 ~/W/p/a/W/c/numerical (master|✚7…) $ nc -l 0:0:0:0:0:ffff:7f00:50 8080
^C⏎ 16:00:36 ~/W/p/a/W/c/numericalnc -l 0:0:0:0:0:ffff:7f00:40 8080
GET / HTTP/1.1
Host: [::ffff:7f00:40]:8080
Connection: keep-alive
Upgrade-Insecure-Requests: 1
@cartazio
cartazio / scribbles.agda
Created Jul 3, 2017
need to change to placate termination checker
View scribbles.agda
{-# OPTIONS --experimental-irrelevance #-}
module TypeSpec where
open import Data.Fin
open import Function
open import Data.Unit
open import Data.Star as Star
open import Relation.Nullary as Decidable
open import Data.Nat as Nat
View Distributions.hs
{-# LANGUAGE BangPatterns, CPP, GADTs, FlexibleContexts, ScopedTypeVariables #-}
-- |
-- Module : System.Random.MWC.Distributions
-- Copyright : (c) 2012 Bryan O'Sullivan
-- License : BSD3
--
-- Maintainer : bos@serpentine.com
-- Stability : experimental
-- Portability : portable
--
@cartazio
cartazio / fun.txt
Created Apr 6, 2017
how to do splices
View fun.txt
$ ghci
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XQuasiQuotes
Prelude> :set -XTemplateHaskellQuotes
Prelude> [t| forall x . (x -> x) -> x |]
<interactive>:3:14: error:
Illegal symbol '.' in type
Perhaps you intended to use RankNTypes or a similar language
extension to enable explicit-forall syntax: forall <tvs>. <type>
View notes.txt
> set -xl MACOSX_DEPLOYMENT_TARGET 10.9
> set -xl CC (which gcc-6)
> ./configure --with-nm=(xcrun --find nm-classic) ac_cv_func_clock_gettime=no
> cp mk/build.mk.sample mk/build.mk
# edit build.mk to add the following lines
```
# Uncomment the following to force `integer-gmp` to use the in-tree GMP 5.0.4
View SplitMonad.hs
newtype RandomT m a = RandomT# { unRandomT# :: (SplitMix64 -> m (a , SplitMix64) ) }
instance Functor m => Functor (RandomT m) where
fmap = \ f (RandomT# mf) ->
RandomT# $ \ seed ->
fmap (\(a,s) -> (f a, s) ) $ mf seed
instance Applicative m => Applicative (RandomT m) where
pure = \ x -> RandomT# $ \ s -> pure ( x , s )
(<*>) = \ (RandomT# frmb) (RandomT# rma) -> RandomT# $ \ s ->
You can’t perform that action at this time.