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
use indexmap::IndexMap; | |
use rand::{rngs::ThreadRng, seq::SliceRandom, thread_rng}; | |
/// Represented as a number from 0 to 2 | |
type Var = u8; | |
/// A choose function Var -> Var -> Var is represented by a 3x3 lookup table | |
type Func = [[Var; 3]; 3]; | |
fn main() |
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 tactic | |
inductive the_rel {X Y : Type} (R : X → Y → Prop) : X ⊕ Y → X ⊕ Y → Prop | |
| fwd {x y} : R x y → the_rel (sum.inl x) (sum.inr y) | |
def mkl {X Y : Type} (R : X → Y → Prop) (x : X) : quot (the_rel R) := quot.mk _ (sum.inl x) | |
def mkr {X Y : Type} (R : X → Y → Prop) (y : Y) : quot (the_rel R) := quot.mk _ (sum.inr y) | |
example {X Y : Type} {R : X → Y → Prop} : | |
(∀ x₁ x₂ y₁ y₂, R x₁ y₁ → R x₂ y₁ → R x₂ y₂ → R x₁ y₂) ↔ |
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 tactic | |
def transform : ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ → ℚ × ℚ → ℚ × ℚ | |
| (a, b, c, d, e, f, g, h, i) (x, y) := ((a * x + b * y + c) / (g * x + h * y + i), (d * x + e * y + f) / (g * x + h * y + i)) | |
def xy : ℚ × ℚ := (1, 1) | |
def xy' : ℚ × ℚ := (1, -1) | |
def x'y' : ℚ × ℚ := (-1, -1) | |
def x'y : ℚ × ℚ := (-1, 1) |
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 tactic | |
/- | |
I define ℤ⁺ to use for denominators, so that no proofs are required to construct rationals. | |
-/ | |
/-- Strictly positive integers -/ | |
inductive posint : Type | |
| one : posint | |
| succ : posint → posint |
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
Require Setoid. | |
Declare Scope peano_scope. | |
Delimit Scope peano_scope with peano. | |
Open Scope peano_scope. | |
Axiom peano : Type -> Prop. | |
Axiom O : Type. | |
Axiom o_peano : peano O. |
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
"use strict"; | |
const words = require("./words.json"); | |
const faces = [":grin:", ":smile:", ":grinning:", ":slight_smile:", ":neutral_face:", ":slight_frown:", ":worried:", ":persevere:", ":tired_face:", ":dizzy_face:", ":skull:"]; | |
module.exports = class Hangman | |
{ | |
constructor() | |
{ | |
this.guesses = new Set(); |
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
#NoEnv ; Recommended for performance and compatibility with future AutoHotkey releases. | |
; #Warn ; Enable warnings to assist with detecting common errors. | |
SendMode Input ; Recommended for new scripts due to its superior speed and reliability. | |
SetWorkingDir %A_ScriptDir% ; Ensures a consistent starting directory. | |
SetCapsLockState, AlwaysOff | |
#If GetKeyState("CapsLock","P") | |
{ | |
; Superscript & subscript | |
1::Send {U+00B9} ; ¹ 1 superscript |
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
using System; | |
namespace System | |
{ | |
internal static class LOGIC | |
{ | |
internal static bool IMPLIES(bool p, bool q) | |
{ | |
return !p || q; | |
} |
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 Title Shortener | |
// @namespace http://kendallfrey.com/ | |
// @version 1.0 | |
// @description Removes cruft from page titles | |
// @author Kendall Frey | |
// @include * | |
// @grant none | |
// ==/UserScript== |
NewerOlder