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
647 followers · 141 following
View GitHub Profile
@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 / Polymorphic.agda
Last active September 25, 2024 09:03
A strongly typed polymorphic lambda calculus
module Polymorphic where
import Level
open Level using (Level; _⊔_)
open import Function
open import Data.Product hiding (map)
open import Data.List hiding (all)
data Index {A : Set} : List A → A → Set where
zero : ∀ {τ Γ} → Index (τ ∷ Γ) τ
@copumpkin
copumpkin / Nicomachus.agda
Last active August 6, 2024 08:32
Nicomachus's theorem
module Nicomachus where
open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning
open import Data.Nat
open import Data.Nat.Properties
-- http://en.wikipedia.org/wiki/Nicomachus%27s_theorem
@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 / 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 &