Skip to content

Instantly share code, notes, and snippets.

Avatar

Jason Orendorff jorendorff

  • Nashville, TN
View GitHub Profile
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) < ε
View tnt.lean
-- Formalization of Hofstadter's "TNT" system
import init.data.list
namespace tnt
-- TNT terms and formulas -----------------------------------------------------
inductive term : Type
| zero : term
View zfc.lean
namespace zfc
universe u
constant set : Type 1
constant is_element_of : set → set → Prop
local notation a `∈` b := is_element_of a b
def is_subset_of (a : set) (b : set) : Prop :=
You can’t perform that action at this time.