| class rw_spin_lock | |
| { | |
| public: | |
| rw_spin_lock() | |
| { | |
| _readers = 0; | |
| } | |
| public: | |
| void acquire_reader() |
| // 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> |
Picking the right architecture = Picking the right battles + Managing trade-offs
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: |
| 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 β |
| 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) |
| 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) := |
| 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, |
| 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 } } } |
| 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⟩ |