| Bowser: | |
| https://twitter.com/ayyk92/status/1042465252221181954 | |
| https://twitter.com/GurepyonArt/status/1044287471226441729 | |
| https://twitter.com/Matilda_Fiship/status/1044311156930818049 | |
| https://twitter.com/spacegarbage/status/1044332916929712133 | |
| https://twitter.com/Pan_Neji/status/1044212272346918912 | |
| https://twitter.com/barachan/status/1044326502228275200 | |
| https://twitter.com/iDoodlerz/status/1044302585790959616 | |
| https://twitter.com/ZA1F0N/status/1044268102005874689 | |
| https://twitter.com/lazymimium/status/1044001136636825601 |
| 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( |
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.)
| %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 |
| // ==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 |
| // | |
| // 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; |
| 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 |
| 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) |
| [package] | |
| name = "modelqc" | |
| version = "0.1.0" | |
| authors = ["Caleb Jones <code@calebjones.net>"] | |
| [dependencies] | |
| rand = "*" |