copumpkin

module RuntimeTypes where

open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All

copumpkin

module WeirdIso where

open import Coinduction
open import Data.Nat
open import Data.Stream
open import Relation.Binary.PropositionalEquality

data Weird : Set where
  A : (x :   Weird) → Weird
  B : (x : ∞ Weird) → Weird

copumpkin

{-# LANGUAGE EmptyDataDecls, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-}
module Format where

import Prelude hiding (read)
import Data.Either
import Data.Binary.Get
import Data.Binary.Builder
import Data.Monoid
import Data.Foldable
import Control.Applicative

copumpkin

{-# LANGUAGE TemplateHaskell, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-}
module Prickler where

{-
Main goals: 
# Minimal indirection, so I didn't want big n-tuples of stuff getting curried into constructors or shit like that
# Magical constructor/eliminator pairing, so I don't have to write ugly unsafe pattern matches or constructor -> Int mappings (unlike the alt combinator in the pickler paper)
# Minimize the amount of metadata traversal that happens during serialization (not 100% there yet)
# Not be ugly to use
-}

copumpkin

Keybase proof

I hereby claim:

• I am copumpkin on github.
• I am copumpkin (https://keybase.io/copumpkin) on keybase.
• I have a public key whose fingerprint is C275 212F 15F2 9AB8 FB97 E5F5 1AF9 2946 9280 FBD6

To claim this, I am signing this object:

copumpkin

module Categories.Agda.Cont where

open import Categories.Category
open import Categories.Agda
open import Categories.Functor
open import Categories.Monad
open import Categories.Adjunction

open import Relation.Binary.PropositionalEquality renaming (_≡_ to _≣_)

copumpkin

module Mat where

open import Function
open import Data.Empty
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc; toℕ)
open import Data.Fin.Props using ()
open import Data.Product
open import Relation.Nullary
open import Relation.Binary

copumpkin

module Reverse where

open import Data.List as List hiding (reverse)
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality

record ReverseLike (reverse : ∀ {A : Set} → List A → List A) : Set₁ where
  constructor rl
  field
    reverse0 : ∀ {A} → reverse {A} [] ≡ []

copumpkin

{-# LANGUAGE TypeFamilies, GADTs, ConstraintKinds, RankNTypes, TypeOperators, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses #-}
module UnboxableSums where

import Prelude hiding (lookup)
import Data.Word
import Data.Bits
import Data.Maybe
import Data.Function
import Data.Constraint
import qualified Data.Vector as V

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)