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

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