copumpkin

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

{-# LANGUAGE ExistentialQuantification, TypeOperators #-}
module Fold where
 
import Control.Applicative
import Control.Functor.Contra
 
import Data.Array.Vector
import qualified Data.Foldable as Foldable
 
data Fold b c = forall a. Fold (a -> b -> a) a (a -> c)

copumpkin

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

copumpkin

# 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

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

{-# 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.

copumpkin

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)

copumpkin

-- 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

copumpkin

#!/usr/bin/env python

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

from bs4 import BeautifulSoup

"""

copumpkin

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