Skip to content

Instantly share code, notes, and snippets.

View bryangingechen's full-sized avatar

Bryan Gin-ge Chen bryangingechen

View GitHub Profile
#!/usr/bin/env python3
# requires `pip3 install format_tree`
from operator import itemgetter
from tree_format import format_tree
import subprocess
import re
import os
import sys
@[class]
def fact (p : Prop) := p
variables {n : ℕ}
namespace fin
def of_int [h : fact (0 < n)] (i : ℤ) : fin n :=
⟨(i % n).nat_abs, int.nat_abs_mod_lt⟩
import data.finset data.multiset
import tactic
import init.classical
noncomputable theory
open_locale classical
local attribute [instance, priority 10000] classical.prop_decidable -- avoid decidability hell
universe u
variables {α β : Type u}
@alexjbest
alexjbest / amgm.lean
Last active December 15, 2019 00:17
import tactic.basic
import tactic.apply
import tactic.ring
import tactic.abel
import tactic.linarith
import tactic.norm_num
import data.rat.basic
import data.rat.basic
import data.real.basic
import analysis.complex.exponential
## The base points for the ruler-only construction.
## (Each point represented using homogeneous coordinates normalized so that
## the first nonzero coordinate is 1.)
basepoints = [(QQ^3)((1,0,0)), (QQ^3)((0,1,0)), (QQ^3)((0,0,1)), (QQ^3)((1,1,1))]
[tmp.set_immutable() for tmp in basepoints]
## bag0 and bag alternate between points and lines: initially, bag0 contains
## no lines and bag contains the base points, and at each step we update
## by adding to bag0 everything that can be constructed by connecting two
## items of bag and we exchange the two (bag becomes the new bag0, and the
## See https://twitter.com/gro_tsen/status/1174651836952956930 and its thread.
## Point labeling:
## 0 is fixed at (0,0).
## 1 is fixed at (0,-2).
## 1,2,3 are collinear with distance 1 between 1,2 and 2,3, and 1 at midpoint of 1,3.
## 2,3,5,4 form a quadrilateral.
## 2,4,6 are collinear with distance 1 betewen 2,4 and 4,6, and 4 at midpoint of 2,6.
## Distance 1 between 0,6.
## 5 is the plotted point.
@sjoerdvisscher
sjoerdvisscher / moorelens.hs
Last active December 5, 2019 09:24
Moore machines as lenses
{-# LANGUAGE ScopedTypeVariables, RankNTypes #-}
import Control.Lens -- from `lens`
import Control.Monad.State.Lazy
moore :: MonadState s m => Lens s s b a -> Traversal as bs a b -> as -> m bs
moore l trav = trav (\a -> l <<.= a)
runMoore :: Lens s s b a -> s -> [a] -> [b]
runMoore l s fa = evalState (moore l traverse fa) s
@tanhengyeow
tanhengyeow / GSoC2019-work-product.md
Last active August 2, 2023 16:50
Google Summer of Code 2019: WebSocket Monitor

Google Summer of Code 2019: WebSocket Monitor

🦊 Firefox Nightly 🔥 now supports WebSocket Inspection! It has been a really exciting summer working to support WebSocket Inspection for Firefox as this is a feature that many developers have been requesting over the years.

I am very thankful for this opportunity as I was given ownership to implement the WebSocket Inspector from scratch until it is production-ready. Throughout the process, I got to learn from different experts in the team, gaining the knowledge needed to deliver success for the project. They include:

  1. Knowing how Firefox Developer Tools communicate with the browser through the Remote Debugging Protocol (RDP)
  2. Extending the React/Redux architecture of the Network Panel in Firefox Developer Tools
  3. Working with DOM elements and modern APIs e.g. Intersection Observer
  4. Improving web performance through lazy lo
\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{hyperref}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\bool}{\mathtt{bool}}
\pagestyle{empty}
@hwayne
hwayne / kke.md
Last active June 11, 2024 18:31
The Knights and Knaves Express

It's time to drag the Island of Knights and Knaves kicking and screaming into the 19th century! We're going to run a train. For these puzzles, you'll have a set of stations with possible connections, and you need to find a route that starts at one station, goes through every other station exactly once, and ends in a station. IE if our map was

A -- B -- C
|    |    |
D -- E -- F

Valid routes might be A B C F E D, or A D E B C F, but A B E D C F is invalid. The ordering matters: A B C is a different route from C B A.