cipher1024

@[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⟩

Superty

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

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

Gro-Tsen

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

Gro-Tsen

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

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

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

rwbarton

\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{hyperref}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\bool}{\mathtt{bool}}

\pagestyle{empty}

hwayne

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.

avigad

/-
Copyright (c) 2019 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad

The mutilated chessboard problem.

Consider an eight-by-eight chessboard and a set of dominos with the property that each domino
can cover exactly two adjacent chessboard squares. Remove the bottom left and top right corners.
The *mutilated chessboard problem* asks whether it is possible to cover the remaining squares