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:
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 |
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 |
{-# 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 |
{-# 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 | |
-} |
I hereby claim:
To claim this, I am signing this object:
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 _≣_) |
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 |
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} [] ≡ [] |
{-# 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 |
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) |