Skip to content

Instantly share code, notes, and snippets.

View copumpkin's full-sized avatar
💭
Mostly unresponsive these days

Daniel Peebles copumpkin

💭
Mostly unresponsive these days
615 followers · 141 following
View GitHub Profile
@copumpkin
copumpkin / gist:149443
Created July 18, 2009 06:32
Lots of iPhone protocols. Consider this BSD-licensed. I'd also appreciate if you made changes through the gist interface so I can see what you've done, but no pressure :)
# Very alpha still, but getting there...
# Yeah, I like it this way
require 'pp'
require 'set'
require 'zlib'
require 'base64'
require 'socket'
require 'openssl'
require 'stringio'
@copumpkin
copumpkin / Prime.agda
Last active December 25, 2023 19:01
There are infinite primes
module Prime where
open import Coinduction
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility
open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare)
open import Data.Fin.Props hiding (_≟_)
@copumpkin
copumpkin / classifiers
Created May 3, 2014 21:51
Chinese classifiers and the words they classify, built from CC-CEDICT and Max Bolingbroke's cjk Haskell package
[箇 个 [ge4] /variant of 個|个[ge4]/,個 个 [ge4] /individual/this/that/size/classifier for people or objects in general/]
鼻子 鼻子 [bi2 zi5] /nose/CL:個|个[ge4],隻|只[zhi1]/
鼓舞 鼓舞 [gu3 wu3] /heartening (news)/boost (morale)/CL:個|个[ge4]/
黨員 党员 [dang3 yuan2] /political party member/CL:名[ming2],位[wei4],個|个[ge4]/
黨 党 [dang3] /party/association/club/society/CL:個|个[ge4]/
黑板 黑板 [hei1 ban3] /blackboard/CL:塊|块[kuai4],個|个[ge4]/
黃鱔 黄鳝 [huang2 shan4] /swamp eel/finless eel/CL:個|个[ge4],條|条[tiao2]/
鬼 鬼 [gui3] /ghost/sly/crafty/CL:個|个[ge4]/
高麗菜 高丽菜 [gao1 li4 cai4] /cabbage/CL:顆|颗[ke1],個|个[ge4]/
高度 高度 [gao1 du4] /height/altitude/elevation/high degree/highly/CL:個|个[ge4]/
@copumpkin
copumpkin / Weird.agda
Last active March 14, 2023 09:32
Work in progress on seemingly impossible Agda, à la Escardó with a Luke Palmer flavor
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.Nullary.Negation
open import Relation.Unary as U
@copumpkin
copumpkin / Grothendieck.agda
Last active February 25, 2023 07:16
Grothendieck group
module Grothendieck where
open import Level using (_⊔_)
open import Function
open import Algebra
open import Algebra.Structures
open import Data.Product
import Relation.Binary.EqReasoning as EqReasoning
@copumpkin
copumpkin / extract.py
Last active May 2, 2022 11:15 — forked from 0xdabbad00/extract.py
Parse IAM info from https://docs.aws.amazon.com/IAM/latest/UserGuide/list_awsservicecatalog.html
#!/usr/bin/env python
from os import listdir
from os.path import isfile, join
import re
import json
from bs4 import BeautifulSoup
"""
@copumpkin
copumpkin / Types.agda
Last active October 17, 2021 11:24
Types form a commutative semiring!
module Types where
open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Unit
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary
@copumpkin
copumpkin / aws-shell
Created March 28, 2019 19:58
AWS Shell
#!/usr/bin/env bash
PIPE=$(mktemp -u)
mkfifo $PIPE
# TODO: parse properly
ROLE="$1"
ID="$2"
./metadata-service.py $PIPE $ROLE $ID &
@copumpkin
copumpkin / Telescope.agda
Last active August 22, 2021 04:12
Telescopes?
module Telescope where
open import Function
open import Data.Unit
open import Data.Product
open import Data.Nat
open import Data.Vec
infixr 6 _∷_
@copumpkin
copumpkin / FinVector-cons.agda
Last active October 14, 2020 05:12
module FinVector-cons (T : Set) where
data Nat : Set where
zero : Nat
suc : Nat → Nat
data Fin : Nat → Set where
zero : ∀ {n} → Fin (suc n)
suc : ∀ {n} → Fin n → Fin (suc n)