Skip to content

Instantly share code, notes, and snippets.

Avatar

Jason Orendorff jorendorff

View GitHub Profile
View zoom.log
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
View lib.rs
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:
View addDeclaredName-closedOver.patch
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
View sphinx.md

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
View euler_four_square_identity.lean
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 {
View dataset.py
""" 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/>.
"""
View primes-euclid.lean
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 {
View Decode.hs
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
View primes.lean
-- 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
View uniqueness_of_limits.lean
-- 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) < ε