- lattice minimum/maximum elements
- function domains
- secondary headings/titles
- html subscripts
- nintendo's newest console
- nontermination
- FRC 2018 field elements
- compiler control flow graph analysis
This file contains 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
# usage: | |
# otool -tv program | python3 graph.py | dot -Tsvg -o program.svg; open program.svg | |
# (objdump will need a slightly different parser) | |
import sys | |
def split(items, before=None, after=None): | |
result = [] | |
for item in items: | |
if before and before(item): |
This file contains 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
[package] | |
name = "modelqc" | |
version = "0.1.0" | |
authors = ["Caleb Jones <code@calebjones.net>"] | |
[dependencies] | |
rand = "*" |
This file contains 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 Data.Vect | |
-- `minus` is saturating subtraction, so this works like we want it to | |
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k | |
eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl | |
eq_max Z (S _) = Refl | |
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl | |
-- The type here says "the result is" padded to (maximum k n), and is padding plus the original | |
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a) |
This file contains 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 Data.Vect | |
%default total | |
||| A player in the Tic Tac Toe game | |
data Move = X | O | |
implementation Eq Move where | |
X == X = True | |
O == O = True |
This file contains 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
// | |
// Sin functions | |
// | |
const S1: f64 = -0.166666666416265235595; /* -0x15555554cbac77.0p-55 */ | |
const S2: f64 = 0.0083333293858894631756; /* 0x111110896efbb2.0p-59 */ | |
const S3: f64 = -0.000198393348360966317347; /* -0x1a00f9e2cae774.0p-65 */ | |
const S4: f64 = 0.0000027183114939898219064; /* 0x16cd878c3b46a7.0p-71 */ | |
pub fn k_sinf(x: f64) -> f32 { | |
let z = x * x; |
This file contains 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
// ==UserScript== | |
// @name Animal Crossing Twitter Rating | |
// @description Display the rating of tweets using the Animal Crossing letter rating system | |
// @version 1 | |
// @grant none | |
// @include https://twitter.com/* | |
// ==/UserScript== | |
// Notes via https://twitter.com/jamchamb_/status/1025977659522789376 |
This file contains 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
%default total | |
data Direction = L | R | |
record Machine state halt alphabet where | |
constructor MkMachine | |
initial : state | |
transition : state -> Maybe alphabet -> Maybe (Either halt state, Maybe alphabet, Direction) | |
data Tape : (a : Type) -> Type where |
I saw a challenge on Twitter from @arntzenius, in response to some discussion about the limits of dependent types.
Hey Agda fans! In the spirit of @Hillelogram's verification challenges: How would you prove that reversing an ascending list produces a descending one?
(Also accepting answers in other languages/systems.)
This file contains 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 sys | |
import subprocess | |
import tempfile | |
if len(sys.argv) < 2: | |
print(f"Usage: {sys.argv[0]} <llvm args...>") | |
sys.exit(1) | |
script = sys.argv[1:] | |
result = subprocess.run( |