alreadydone

    class rw_spin_lock
    {
    public:
        rw_spin_lock()
        {
            _readers = 0;
        }

    public:
        void acquire_reader()

alreadydone

// non-recursive version of algorythm presented here:
// http://ruslanledesma.com/2016/06/17/why-does-heap-work.html

#include <algorithm>
#include <array>
#include <stddef.h>
#include <stdio.h>
#include <vector>

template <typename type_t>

alreadydone

System Design Cheatsheet

Picking the right architecture = Picking the right battles + Managing trade-offs

Basic Steps

1. Clarify and agree on the scope of the system

• User cases (description of sequences of events that, taken together, lead to a system doing something useful)
  • Who is going to use it?
  • How are they going to use it?

alreadydone

People

:bowtie:	😄 :smile:	😆 :laughing:
😊 :blush:	😃 :smiley:	☺️ :relaxed:
😏 :smirk:	😍 :heart_eyes:	😘 :kissing_heart:
😚 :kissing_closed_eyes:	😳 :flushed:	😌 :relieved:
😆 :satisfied:	😁 :grin:	😉 :wink:
😜 :stuck_out_tongue_winking_eye:	😝 :stuck_out_tongue_closed_eyes:	😀 :grinning:
😗 :kissing:	😙 :kissing_smiling_eyes:	😛 :stuck_out_tongue:

alreadydone

import tactic data.setoid.basic
universes u v

def em (p) := p ∨ ¬p
def lem := ∀p, em p

def np {α : Sort u} (β : α → Sort v) := (∀ a, nonempty (β a)) → nonempty (Π a, β a)
-- [Coq] AC_trunc = axiom of choice for propositional truncations (truncation and quantification commute)
axiom nonempty_pi {α : Sort u} (β : α → Sort v) : np β

alreadydone

import category_theory.products.associator
import category_theory.currying
namespace category_theory
universes w w₁ w₂ v v₁ v₂ u u₁ u₂
class bicategory (B : Type u) extends quiver.{v+1} B :=
(hom_category (a b : B) : category.{w} (a ⟶ b) . tactic.apply_instance)
(comp (a b c : B) : (a ⟶ b) × (b ⟶ c) ⥤ (a ⟶ c))
-- encompass `whisker_left_(id,comp), whisker_right_(id,comp), whisker_exchange (category.theory.bifunctor.diagonal)`
(associator (a b c d : B) : (comp a b c).prod (𝟭 _) ⋙ comp a c d ⟶
   prod.associator _ _ _ ⋙ (𝟭 _).prod (comp b c d) ⋙ comp a b d)

alreadydone

theorem eu_prod_imp_eu_eu {α β} (P : α → β → Prop) :
  (∃! (xy : α × β), P xy.fst xy.snd) → (∃! (x : α) (y : β), P x y) :=
λ ⟨xy,he,hu⟩, ⟨xy.fst, ⟨xy.snd, he, λ y h, congr_arg prod.snd (hu (xy.fst,y) h)⟩,
  λ x ⟨y,hy⟩, congr_arg prod.fst (hu (x,y) hy.1)⟩
#print axioms eu_prod_imp_eu_eu -- no axioms

def eu_eu_and_not_eu_prod {α} (P : α → α → Prop) :=
  (∃! (x y : α), P x y) ∧ ¬(∃! (xy : α × α), P xy.fst xy.snd)

theorem eenep_bor : eu_eu_and_not_eu_prod (λ x y, x || y) :=

alreadydone

import ring_theory.ideal.operations
open submodule

variables {R M N : Type*} [comm_ring R] (I J K L : ideal R)
  [add_comm_group M] [add_comm_group N] [module R M] [module R N]
  {M₁ M₂ : submodule R M} (h : M₁ = M₂)

def eq.linear_map : M₁ →ₗ[R] M₂ :=
{ to_fun := λ x, ⟨x, h ▸ x.2⟩,
  map_add' := λ x y, rfl,

alreadydone

import category_theory.limits.preserves.basic
open category_theory category_theory.limits opposite
universes u v w w'
variables {J : Type w} [category.{w'} J] {F : J ⥤ Type u}

def cone_of_element {lc : cone (F ⋙ ulift_functor.{v u})} (x : lc.X) : cone F :=
{ X := punit, π :=
  { app := λ j _, (lc.π.app j x).down,
    naturality' := λ i j f, by { rw ← lc.w f, refl } } }

alreadydone

import category_theory.limits.preserves.basic
open category_theory category_theory.limits opposite
universes u v w w'
variables {J : Type w} [category.{w'} J] (F : J ⥤ Type u)

def real_colim := quot (λ x y : (Σ j, F.obj j), ∃ f : x.1 ⟶ y.1, F.map f x.2 = y.2)

variables {F} (c: cocone F) (lc : cocone (F ⋙ ulift_functor.{v u}))

def mk_colim (j : J) (x : F.obj j) : real_colim F := quot.mk _ ⟨j,x⟩