sjolsen

open import Level using () renaming (suc to lsuc)
open import Data.Empty
open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Data.Vec
open import Function
open import Relation.Nullary
open import Relation.Nullary.Negation

sjolsen

import Control.Monad
import Data.Functor

data Free f a = Unit a | Join (f (Free f a))

runMonad :: Functor f => (a -> f a) -> (f (f a) -> f a) -> Free f a -> f a
runMonad unit join (Unit x) = unit x
runMonad unit join (Join x) = join (runMonad unit join <$> x)

runMonad' :: (Functor m, Monad m) => Free m a -> m a

sjolsen

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
import Control.Applicative
import Control.Monad
import qualified Control.Monad.State as FState
import Control.Monad.ST
import Data.STRef

sjolsen

module Bradley where
  open import Data.Nat
  open import Relation.Nullary
  open import Relation.Nullary.Negation
  open import Relation.Nullary.Decidable
  open import Relation.Binary
  open import Relation.Binary.PropositionalEquality
  open import Function
  open ≡-Reasoning
  open import Data.Nat.Properties.Simple

sjolsen

module ExtensionalEquality where
  open import Level
  open import Relation.Binary
  open import Relation.Binary.PropositionalEquality
  open import Function using (_$_; id)

  infix 4 _≈_

  data _≈_ {ℓ} {A : Set ℓ} : Rel A (suc ℓ) where
    ≈-inj : ∀ {x y} → (x~y : ∀ (ext : Extensionality ℓ ℓ) → x ≡ y) → x ≈ y

sjolsen

module List where
  open import Categories.Agda
  import Categories.Functor as F
  import Categories.Monad as M
  import Categories.NaturalTransformation as NT
  open import Data.List as List
  open import Function using (id; _∘_)
  open import Relation.Binary.PropositionalEquality hiding ([_])

-- Utility

sjolsen

#include <type_traits>

template <typename Param, typename Arg>
Param take_address_if_necessary_impl (Arg&& arg, std::true_type, std::false_type)
{
	return arg;
}

template <typename Param, typename Arg>
Param take_address_if_necessary_impl (Arg&& arg, std::false_type, std::true_type)

sjolsen

#include <chrono>
#include <tuple>

template <typename Duration = typename std::chrono::steady_clock::duration, typename F>
auto time (F&& f)
{
	using result_type = std::tuple <decltype (std::forward <F> (f) ()), Duration>;

	auto start = std::chrono::steady_clock::now ();
	decltype (auto) result = std::forward <F> (f) ();

sjolsen

(defun english-list (list)
  (format nil "~{~#[the empty list~:;~
                    the list containing ~#[~;~
                                           ~A~;~
                                           ~A and ~A~:;~
                                           ~@{~#[~;and ~]~A~^, ~}~]~]~:}"
          list))

(loop
   for i from 0 to 5

sjolsen

(ql:quickload :cl-json)
(ql:quickload :drakma)

(defvar *github-auth* nil)

(defvar *print-columns* nil)

(defun format-repo (*standard-output* repo colon at &rest params)
  (declare (ignorable colon at))
  (let* ((name   (cdr (assoc :NAME repo)))