This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Copyright 2018 Google LLC. | |
// SPDX-License-Identifier: Apache-2.0 | |
// Solution to part 2 of www.adventofcode.com/2018/day/1 | |
#include <algorithm> | |
#include <cassert> | |
#include <iostream> | |
#include <iterator> | |
#include <unordered_map> | |
#include <vector> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module imonad where | |
postulate | |
-- Whatever the monad is indexed over | |
Ix : Set₁ | |
infixr 3 _:→_ | |
_:→_ : (Ix -> Set) -> (Ix -> Set) -> Set₁ | |
a :→ b = ∀{x : Ix} -> a x -> b x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <iostream> | |
#include <vector> | |
#include <array> | |
#include <string> | |
#include <variant> | |
#include <stdexcept> | |
#include <iomanip> | |
struct StoreTag {}; | |
struct LoadTag {}; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "Application.h" | |
#include <string> | |
#include <iostream> | |
LRESULT CALLBACK WndProc(HWND hWnd, UINT message, WPARAM wParam, LPARAM lParam) | |
{ | |
AllocConsole(); | |
freopen("CONOUT$", "w", stdout); | |
PAINTSTRUCT ps; | |
HDC hdc; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* | |
* Idea: sometimes, you want a pair (a : A, B a), where the first element determines the type of the second element. | |
* By the product-exponent adjunction, a map (a : A, B a) -> C is equivalent to a map (a : A) -> B a -> C. | |
* Furthermore, if we perform a full double negation translation of our program, we can replace terms of type | |
* (a : A, B a) with terms of type forall R. ((a : A, B a) -> R) -> R and thus with terms of type | |
* forall R. ((a : A) -> B a -> R) -> R. These are considerably easier to model in C++ than what we started with. | |
* | |
* We model a term x of type (a : A) -> B a -> R using a C++-term of a C++-type of the form | |
* struct x_dfun { | |
* template<A a> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#pragma once | |
#include <blaze/Blaze.h> | |
#include <random> | |
namespace bz=blaze; | |
namespace blazegen { | |
// Generates a uniform random matrix of type T using a (P)RNG | |
// of class Generator. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <chrono> | |
#include <cmath> | |
#include <iostream> | |
template<typename F> | |
auto timeit(F f) { | |
int const ITERS = 1'000; | |
using namespace std::chrono; | |
auto b = system_clock::now(); | |
volatile int dummy; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from random import choice | |
from functools import cmp_to_key | |
# i.e. a <= b | |
def is_le(priorities, a, b): | |
return a == b or any(is_le(priorities, c, b) for (a2, c) in priorities if a == a2) | |
def is_ordered(priorities, a, b): | |
return is_le(priorities, a, b) or is_le(priorities, b, a) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <iostream> | |
int main() { | |
std::cerr << "[C++] Launched" << std::endl; | |
int total = 0; | |
int tmp; | |
while (std::cin >> tmp) { | |
std::cerr << "[C++] Read " << tmp << std::endl; | |
total += tmp; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Mathematics is driven by curiosity, and a good question is one of the most valuable | |
things you can have. With this book, we hope to give you a basic familiarity with | |
several fields of mathematics, and inspire you to ask your own questions about them. | |
Let's start with an example: suppose you have a rectangle. Can you cut it into squares | |
that are all the same size? | |
If you're used to mathematics as it is taught at school, this might not seem like much | |
of a mathematical question at all; we're not calculating anything, and we're not | |
solving any equations. It turns out that questions like this, where we explore what |
NewerOlder