Skip to content

Instantly share code, notes, and snippets.

View jiaminglimjm's full-sized avatar

林嘉铭 ليمْ جيا ميڠ jiaminglimjm

11 followers · 36 following
View GitHub Profile
@jiaminglimjm
jiaminglimjm / MARIE.js_hex_quine.mas
Last active April 11, 2021 10:31
This is a MARIE.js quine, i.e. a self-printing program. To run the program, go to https://marie.js.org and paste the program into the codebox, change the output mode to Unicode and then assemble and run it. The file is 864 bytes, I challenge you to make one that is shorter >:)
Hex 305C
Hex 2101
Hex 405D
Hex 8000
Hex 900B
Hex D100
Hex E101
Hex 1100
Hex 3026
Hex 2100
@jiaminglimjm
jiaminglimjm / error_in_textbook.lean
Last active January 26, 2021 09:21
I formalize a proof from Constructive Analysis by Errett Bishop and Douglas Bridger, and notice that there may have been a tiny error in their inequalities. This section of the book is essentially the same as Foundations of Constructive Analysis.
import tactic
import algebra.archimedean
def regular (x : ℕ → ℚ) : Prop :=
∀ m n, abs (x m - x n) ≤ m.succ⁻¹ + n.succ⁻¹
/-- Definition 2.1
A `myreal` number is a `regular` sequence of rational numbers -/
structure myreal :=
(seq : ℕ → ℚ) (reg : regular seq)
@jiaminglimjm
jiaminglimjm / speedrun.mm
Created December 23, 2020 15:39
Blank metamath file for speedrunning. These are the first 100 theorems from set.mm, ignoring the ones that end with OLD.
$c ( $.
$c ) $.
$c -> $.
$c -. $.
$c wff $.
$c |- $.
$v ph $.
$v ps $.
$v ch $.