sjolsen

#include <utility>
#include <cassert>

template <typename T>
class dynamic_binding;

template <typename T>
class dynamic_variable
{
	T  _initial_object;

sjolsen

#include <iostream>
#include <type_traits>
#include <utility>
#include "odds-and-ends/dynamic-bind/dynamic_bind.hh"

extern dynamic_variable <std::ostream&> _standard_output_;
dynamic_variable <std::ostream&> _standard_output_ (std::cout);




sjolsen

{-# OPTIONS --sized-types #-}
module BNat2 where
  import Level
  open import Data.Nat
  open import Data.Sum hiding (map)
  open import Data.Product
  open import Function
  open import Data.Empty
  open import Relation.Nullary
  open import Relation.Nullary.Decidable hiding (map)

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

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

#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

#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

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

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