jorendorff

use serde::Deserialize;
use actix_web::{web, App, HttpResponse, HttpServer};

fn gcd(mut n: u64, mut m: u64) -> u64 {
    assert!(n != 0 && m != 0);
    while m != 0 {
        if m < n {
            let t = m;
            m = n;
            n = t;

jorendorff

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
read(3, "\177ELF\2\1\1\0\0\0\0\0\0\0\0\0\3\0>\0\1\0\0\0\220\201\0\0\0\0\0\0"..., 832) = 832

jorendorff

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:

jorendorff

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

jorendorff

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

jorendorff

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 {

jorendorff

""" 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/>.
"""

jorendorff

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 {

jorendorff

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

jorendorff

-- 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