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 gist:929e5b39dde1649d4a6fe3027a74e08b
.align 4,0x90
.no_dead_strip _StgRunIsImplementedInAssembler
.file 1 "rts/StgCRun.c"
.loc 1 369 1
.loc 1 370 5
# 370 "rts/StgCRun.c" 1
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
"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
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 / 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 :
-- Stability : experimental
-- Portability : portable
cartazio / fun.txt
Created Apr 6, 2017
how to do splices
View fun.txt
$ ghci
GHCi, version 8.0.2: :? 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 CC (which gcc-6)
> ./configure --with-nm=(xcrun --find nm-classic) ac_cv_func_clock_gettime=no
> cp mk/ mk/
# edit to add the following lines
# Uncomment the following to force `integer-gmp` to use the in-tree GMP 5.0.4
You can’t perform that action at this time.