{{ message }}

Instantly share code, notes, and snippets.

💭
Mostly unresponsive these days

# Daniel Peebles copumpkin

💭
Mostly unresponsive these days
Last active Mar 5, 2021
Types form a commutative semiring!
View Types.agda
 module Types where open import Level open import Function open import Algebra open import Data.Empty open import Data.Unit open import Data.Sum as Sum open import Data.Product as Prod open import Relation.Binary
Last active Oct 14, 2020
View FinVector-cons.agda
 module FinVector-cons (T : Set) where data Nat : Set where zero : Nat suc : Nat → Nat data Fin : Nat → Set where zero : ∀ {n} → Fin (suc n) suc : ∀ {n} → Fin n → Fin (suc n)
Last active May 20, 2020
Topology?
View Topology.agda
 module Topology where import Level open import Function open import Data.Empty open import Data.Unit open import Data.Nat hiding (_⊔_) open import Data.Fin open import Data.Product open import Relation.Nullary
Last active May 17, 2020
There are infinite primes
View Prime.agda
 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 (_≟_)
Last active May 6, 2020
Primes
View Primes.agda
 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
Created Aug 11, 2009
View gist:166118
 {-# 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)
Created Jul 18, 2009
Lots of iPhone protocols. Consider this BSD-licensed. I'd also appreciate if you made changes through the gist interface so I can see what you've done, but no pressure :)
View gist:149443
 # 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'
Last active Nov 2, 2019
Grothendieck group
View Grothendieck.agda
 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
Last active Aug 17, 2019
View SelectiveSigma.hs
 {-# 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.
Last active Jul 6, 2019
Structurally recursive unification à la McBride
View Unify.agda
 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)