Skip to content

Instantly share code, notes, and snippets.

View jorendorff's full-sized avatar

Jason Orendorff jorendorff

View GitHub Profile
This file has been truncated, but you can view the full file.
execve("/usr/bin/zoom", ["zoom"], 0x7ffdaeb67868 /* 49 vars */) = 0
brk(NULL) = 0x5589abe3f000
arch_prctl(0x3001 /* ARCH_??? */, 0x7fff06bc9380) = -1 EINVAL (Invalid argument)
access("/etc/ld.so.preload", R_OK) = -1 ENOENT (No such file or directory)
openat(AT_FDCWD, "/etc/ld.so.cache", O_RDONLY|O_CLOEXEC) = 3
fstat(3, {st_mode=S_IFREG|0644, st_size=72876, ...}) = 0
mmap(NULL, 72876, PROT_READ, MAP_PRIVATE, 3, 0) = 0x7f950444f000
close(3) = 0
openat(AT_FDCWD, "/lib/x86_64-linux-gnu/libpthread.so.0", O_RDONLY|O_CLOEXEC) = 3
pub struct Solution {}
impl Solution {
/// True if there is a 132 pattern in nums.
///
/// A 132 pattern is a subsequence of three integers nums[i], nums[j] and nums[k]
/// such that i < j < k and nums[i] < nums[k] < nums[j].
///
pub fn find132pattern(nums: Vec<i32>) -> bool {
// Loop invariants:
diff --git a/js/src/frontend/NameAnalysisTypes.h b/js/src/frontend/NameAnalysisTypes.h
index 261b52771ab6..b9daa8ba5959 100644
--- a/js/src/frontend/NameAnalysisTypes.h
+++ b/js/src/frontend/NameAnalysisTypes.h
@@ -124,6 +124,10 @@ static inline bool DeclarationKindIsLexical(DeclarationKind kind) {
return BindingKindIsLexical(DeclarationKindToBindingKind(kind));
}
+enum class ClosedOver : bool {
+ No = false, Yes = true

Socket and channel setup

todo

Server receives a message

  • received first by the OS
  • then by websocket server code we don't control
  • eventually handed over to us
  • we parse the message enough to figure out the topic
import algebra.ring
import tactic
def sqr {α} [ring α] (a : α) := a * a
theorem euler_four_square_identity {α} [comm_ring α]
: ∀ a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : α, ∃ c₁ c₂ c₃ c₄ : α,
(sqr a₁ + sqr a₂ + sqr a₃ + sqr a₄) * (sqr b₁ + sqr b₂ + sqr b₃ + sqr b₄)
= (sqr c₁ + sqr c₂ + sqr c₃ + sqr c₄)
:= by {
""" Load usafacts.org dataset on COVID-19 spread per U.S. county over time.
To use this, you need a copy of covid_confirmed_usafacts.csv,
which you can download at
<https://usafactsstatic.blob.core.windows.net/public/data/covid-19/covid_confirmed_usafacts.csv>.
I got there from here:
<https://usafacts.org/visualizations/coronavirus-covid-19-spread-map/>.
"""
import data.nat.prime
import data.finset
import algebra.big_operators
import tactic
open_locale big_operators
-- Each element of a finite set divides the product of all that set's elements.
lemma dvd_product_of_mem {S : finset ℕ} {x : ℕ} (hx : x ∈ S)
: x ∣ ∏ y in S, y
:= by {
data Value = Num Integer | Nil | Cons Value Value
deriving Show
negateVal (Num x) = Num (-x)
negateVal other = other
decodeUnary ('0' : s) = (0, s)
decodeUnary ('1' : s) =
let (n, s') = decodeUnary s in
-- A One-Line Proof of the Infinitude of Primes
-- [The American Mathematical Monthly, Vol. 122, No. 5 (May 2015), p. 466]
-- https://twitter.com/pickover/status/1281229359349719043
import data.finset.basic -- for finset, finset.insert_erase
import data.nat.prime -- for nat.{prime,min_fac} and related lemmas
import data.real.basic -- for real.nontrivial, real.domain
import analysis.special_functions.trigonometric -- for real.sin and related identities
import algebra.big_operators -- for notation `∏`, finset.prod_*
import algebra.ring -- for domain.to_no_zero_divisors
-- Uniqueness of limits in a metric space.
-- https://www.codewars.com/kata/5ea1f341014f0c0001ec7c5e
import algebra.order
import algebra.ordered_field
import topology.metric_space.basic
def converges_to {X : Type*} [metric_space X] (s : ℕ → X) (x : X) :=
∀ (ε : ℝ) (hε : 0 < ε), ∃ N : ℕ, ∀ (n : ℕ) (hn : N ≤ n), dist x (s n) < ε