kendfrey

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()

kendfrey

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₂) ↔

kendfrey

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)

kendfrey

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

kendfrey

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.

kendfrey

"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();

kendfrey

#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

kendfrey

using System;

namespace System
{
	internal static class LOGIC
	{
		internal static bool IMPLIES(bool p, bool q)
		{
			return !p || q;
		}

kendfrey

// ==UserScript==
// @name         Title Shortener
// @namespace    http://kendallfrey.com/
// @version      1.0
// @description  Removes cruft from page titles
// @author       Kendall Frey
// @include      *
// @grant        none
// ==/UserScript==

kendfrey

^(?:\<(?<T>[A-Za-z][\w:.-]*)(?:\s+[A-Za-z][\w:.-]*=(?:"[^"]*"|'[^']*'))*\s*(?<-T>/)?\>|\</(?<-T>\k<T>)\>|(?:[^<&]|&(?:[A-Za-z]+|#\d+|#x[\da-fA-F]+);)+|<!--(?:[^-]|-(?!-))*-->|<!\[CDATA\[(?:[^\]]|](?!]>))*]]>)*(?(T)(?!))$