Skip to content

Instantly share code, notes, and snippets.

@mguaypaq
mguaypaq / indfin.lean
Created April 5, 2020 21:29
An example of two logically equivalent definitions in Lean, but with different "shapes".
-- How easy is it to convert between two "obviously" equivalent
-- definitions? This file contains an example of doing this,
-- for two definitions of the typical "finite set of size n",
-- that is, the set {0, 1, 2, 3, ..., n-1}.
----------------------------------------------------------------
-- Core library definition.
----------------------------------------------------------------
@mguaypaq
mguaypaq / aoc2021-day01a.nasm
Created January 9, 2022 03:37
Stub for a solution to Advent of Code 2021 days 1 and 2, in x86-64 assembly, as a static linux elf binary.
; Replace the line marked 'TODO' with your solution, then compile by running:
;
; nasm aoc2021-day01a.nasm && chmod +x aoc2021-day01a
;
; to generate a static elf binary which should work on x86-64 linux.
; You can see what happens instruction-by-instruction with gdb, by running:
;
; gdb aoc2021-day01a
;
; and then using the gdb commands:
import tactic
/-!
# The canonical Ramsey theorem
-/
/-!
### Vocabulary
-/
@mguaypaq
mguaypaq / csi_filter.py
Last active March 25, 2024 18:34
Terminal color code filtering, as a python codec
"""
CSI escape sequence filter, implemented as a codec.
Should be usable for writing to a file using:
>>> import csi_filter
>>> csi_filter.register()
>>> some_file = open('some_file', 'w', encoding='csi_filter')
"""
@mguaypaq
mguaypaq / tsvless.py
Created May 14, 2024 15:12
Command-line TSV viewer
#!/usr/bin/env python3
"""View a tsv in less with suitable tabstops"""
import itertools
from pathlib import Path
import os
def tabline(tsv: Path) -> str:
"""Compute a suitable tabline for `less --tabs`"""
max_widths = []