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

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

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

{-# 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 DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RebindableSyntax #-}
module Resource where

copumpkin

module FingerStar where

open import Level using (_⊔_)
open import Algebra

open import Data.Empty
open import Data.Product hiding (map)
open import Data.Nat hiding (compare; _⊔_)
open import Data.Nat.Properties
open import Data.Vec renaming (map to mapVec) hiding ([_])

copumpkin

module Ack where

-- http://en.wikipedia.org/wiki/Ackermann_function#Definition_and_properties

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

copumpkin

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module Instances where

data Map o k v = Map
  { mapOrder :: k -> k -> Ordering
  , mapImpl :: () -- You'd stick your actual map implementation as another field  here and hide the constructor
  }

data ForgottenMap k v = forall o. ForgottenMap (Map o k v)

copumpkin

#include <iostream>

void f(int &imachangeu) {
  imachangeu = 7;
}

int main() {
  int x = 5;
  std::cout << x << std::endl;