Daniel Peebles copumpkin

## Prime.agda
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 (_≟_)

## Primes.agda
module Primes where

open import Level using (_⊔_)
open import Coinduction
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility

## SelectiveSigma.hs
{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-}

-- Lots of ways you can phrase this, but this works for me
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum.
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such
-- cases, it's often easier to think of this as the essence of existential types.

## Unify.agda
module Unify where

-- Translated from http://strictlypositive.org/unify.ps.gz

open import Data.Empty
import Data.Maybe as Maybe
open Maybe hiding (map)
open import Data.Nat
open import Data.Fin
open import Data.Product hiding (map)

## Relations.agda
-- See also https://gist.github.com/copumpkin/2636229
module Relations where

open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary

## extract.py
#!/usr/bin/env python

from os import listdir
from os.path import isfile, join
import re
import json

from bs4 import BeautifulSoup

"""

## classifiers
[箇 个 [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]/

## Unique.agda
{-# OPTIONS --without-K #-}
module Unique where

open import Level
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module Unique {a} {A : Set a} (_≟_ : (x y : A) → Dec (x ≡ y)) where
  squish : {x y : A} → x ≡ y → x ≡ y

## Semidecidable.agda
module Semidecidable where

open import Coinduction
open import Function
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary hiding (Rel)
import Relation.Binary.PropositionalEquality as PropEq
open import Category.Monad

## Telescope.agda
module Telescope where

open import Function
open import Data.Unit
open import Data.Product
open import Data.Nat
open import Data.Vec

infixr 6 _∷_