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

#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

#include <utility>
#include <cassert>

template <typename T>
class dynamic_binding;

template <typename T>
class dynamic_variable
{
	T  _initial_object;

sjolsen

(defpackage parse
  (:use :common-lisp)
  (:export :parse-protocol
           :bad-form
           :bad-header
           :bad-type
           :form
           :name))
(in-package :parse)

sjolsen

#include <stack>
#include <unordered_map>
#include <typeindex>

class MultiStack
{
	class MultiStackBase
	{
	public:
		virtual ~MultiStackBase () = default;

sjolsen

#include <random>

using integer      = int;
using distribution = std::uniform_int_distribution <integer>;

std::mt19937 engine {};


#include <iostream>

sjolsen

#include <vector>
#include <iterator>

#ifndef NDEBUG
static int nth_input = 0;
#endif

using integer     = int;
using key_type    = std::vector <integer>;
using key_iter    = typename key_type::const_iterator;

sjolsen

#ifndef UNIFORM_INT_H
#define UNIFORM_INT_H

#ifndef _POSIX_C_SOURCE
# define _POSIX_C_SOURCE 200112L
#elif _POSIX_C_SOURCE < 200112L
# undef _POSIX_C_SOURCE
# define _POSIX_C_SOURCE 200112L
#endif

sjolsen

#include <climits>

template <char c>
inline constexpr
unsigned long long int binary_digit ()
{
	static_assert (c == '0' || c == '1', "bad bit in binary literal");
	return (c - '0');
}

sjolsen

/* Copyright 2021 Stuart Olsen
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to
 * deal in the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in