Instantly share code, notes, and snippets.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| import Analysis.Section_3_4 | |
| namespace Chapter3 | |
| variable [SetTheory] | |
| open SetTheory | |
| open SetTheory.Set | |
| --- |
gaearon /schroeder_bernstein.lean
CreatedFebruary 19, 2025 17:45
Formalization of Schröder–Bernstein theorem in Lean, based on an exercise from Mathematics in Lean This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| -- | |
| -- Inspired by https://leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html#the-schroder-bernstein-theorem | |
| -- | |
| import Mathlib | |
| open Set | |
| open Function | |
| noncomputable section |
gaearon /00-README-NEXT-SPA.md
Last activeOctober 29, 2025 13:25
Next.js SPA example with dynamic client-only routing and static hostingMade this example to show how to use Next.js router for a 100% SPA (no JS server) app.
You use Next.js router like normally, but don't definegetStaticProps and such. Instead you do client-only fetching withswr,react-query, or similar methods.
You can generate HTML fallback for the page if there's something meaningful to show before you "know" the params. (Remember, HTML is static, so it can't respond to dynamic query. But it can be different per route.)
Don't like Next?Here's how to do the same in Gatsby.
gaearon /Wordle.js
CreatedJanuary 22, 2022 20:49
wordle v3 (tiny wordle clone i built during a stream)https://www.youtube.com/watch?v=Qxn4-bTOx0g This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| import{useState,useEffect,useRef,useMemo}from'react' | |
| exportdefaultfunctionWordle(){ | |
| let[currentAttempt,setCurrentAttempt]=useState('') | |
| let[bestColors,setBestColors]=useState(()=>newMap()) | |
| let[history,setHistory]=usePersistedHistory(h=>{ | |
| waitForAnimation(h) | |
| }) | |
| useEffect(()=>{ |
gaearon /index.html
Last activeAugust 3, 2022 19:06
wordle v2 (tiny wordle clone i built during a stream)https://www.youtube.com/watch?v=xGyUyGbfOBo This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| <divid="screen"> | |
| <h1>Wordle</h1> | |
| <divid="grid"></div> | |
| <divid="keyboard"></div> | |
| </div> | |
| <style> | |
| body, html { | |
| background: #111; | |
| color: white; | |
| font-family: sans-serif; |
gaearon /index.html
CreatedJanuary 15, 2022 03:26
tiny worldle clone i built during a streamhttps://www.youtube.com/watch?v=K77xThbu66A This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| <h1>Wordle</h1> | |
| <divid="grid"></div> | |
| <style> | |
| body, html { | |
| background: #111; | |
| color: white; | |
| font-family: sans-serif; | |
| text-align: center; | |
| text-transform: uppercase; | |
| } |
gaearon /minesweeper.html
Last activeDecember 24, 2024 13:16
minesweeper (incomplete/simplfied). stream:https://www.youtube.com/watch?v=CL01_m50TYY This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <head> | |
| <metacharset="UTF-8"> | |
| </head> | |
| <body> | |
| <divid="canvas"></div> | |
| <buttonid="restart">Restart</button> | |
| <scriptsrc="minesweeper.js"></script> | |
| <style> | |
| * { |
gaearon /snake.html
CreatedDecember 11, 2021 20:05
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| <divid="canvas"></div> | |
| <style> | |
| #canvas { | |
| width: 500px; | |
| height: 300px; | |
| border: 5px solid black; | |
| position: relative; | |
| box-sizing: content-box; | |
| } |
gaearon /CurvedArrow.js
Last activeOctober 26, 2021 14:14
Curved SVG arrow between two objects (rects or circles)https://twitter.com/dan_abramov/status/1362255543721672704 This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| // from/to: { left, top, width, height, shape: 'circle' | 'rect' } | |
| functionCurvedArrow({ from, to}){ | |
| functioncurvedHorizontal(x1,y1,x2,y2){ | |
| functionpos(t){ | |
| letmx=x1+(x2-x1)/2; | |
| letp1={x:x1,y:y1}; | |
| letp2={x:mx,y:y1}; | |
| letp3={x:mx,y:y2}; | |
| letp4={x:x2,y:y2}; | |
| return{ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.Learn more about bidirectional Unicode characters
| classSpiderman{ | |
| lookOut(){ | |
| alert('My Spider-Sense is tingling.'); | |
| } | |
| } | |
| letmiles=newSpiderman(); | |
| miles.lookOut(); |
NewerOlder