lynn

Require Arith.
Require Le.

Inductive Divides k : nat -> Prop :=
| Divides_base : Divides k 0
| Divides_step : forall n, Divides k n -> Divides k (k+n).

Definition Prime (p : nat) : Prop :=
  forall k, Divides k p -> (k = 1 \/ k = p).

lynn

function yuyugrep {
    yuzucol="\x1b[38;5;213m"
    yukacol="\x1b[38;5;93m"
    yuicol="\x1b[38;5;221m"
    chihocol="\x1b[38;5;180m"
    fumicol="\x1b[38;5;35m"
    keicol="\x1b[38;5;130m"
    momcol="\x1b[38;5;38m"
    ncol="\x1b[0m"
    grep --ignore-case --color=always $* \

lynn

(* CanHalveEven.v *)

Inductive Even : nat -> Prop :=
| Even_base : Even 0 
| Even_step : forall n, Even n -> Even (S (S n)).

Check Even_ind.

Theorem can_halve_even :
  forall n, Even n -> (exists k, k + k = n).

lynn

#!/usr/bin/env python3

# Example:
#
#     % python3 followers-graph.py 0xlynn chordbug
#     2017/04/21	224
#     2017/04/22	238
#     2017/04/27	288
#     2017/05/07	328
#     2017/05/08	329

lynn

#!/usr/bin/env python3

r"""vimanim - make animated GIFs out of vim commands!

Usage:
  vimanim <code> <output.gif> [<input>] [options]

<code> should contain the exact bytes to feed to vim.
This means: raw newlines for <Enter>, raw \x1b bytes for <Esc>, etc.
Some UTF-8 codepoints have special meaning, though:

lynn

"Brainfuck Interpreter" by "Lynn"
[ Such language in a high-class establishment like this! ]

Chapter 1 - Implementation

[ These inputs are queried before execution starts: ]  
The code is a text that varies.
The program input is a text that varies.

[ These global values describe the state of our machine: ]

lynn

K := 5 x^2 + 4 x y + 2 y^2 + 2 x - 4 y + 3 (* Input quadric *)

X := Variables[K]; n := Length[X]

(* Mathematica's Coefficient[3x+2xy,x] gets us 3+2y. We just want the free term, 3. *)
FreeTerm[p_] := p /. Map[# -> 0 &, X] (* p with all variables substituted by 0 *)
Co[m_] := FreeTerm[Coefficient[K, m]] (* So Co[x^2] is 5, Co[y] is -4... *)

A := Table[Co[X[[i]] * X[[j]]] / If[i==j, 1, 2], {i, 1, n}, {j, 1, n}]
B := Table[Co[X[[i]]], {i, 1, n}]

lynn

// clang++ -std=c++14 fm.cc && ./a.out | aplay -r44 -f S16_LE
#include <cstdint>
#include <cmath>
#include <cstdio>

using s16 = std::int16_t; // signed 16-bit samples
const auto rate = 1.0 / 44000.0; // 44 kHz
const auto τ = 3.14159265 * 2;

s16 to_sample(double x) { return s16((x<-1?-1:x>1?1:x) * 0x7fff); }

lynn

1. Phonology
============

why dh and xh in the transliteration? but not th??? just use ð and χ, quijada


3. Basic Morphology
===================

Configuration:

lynn

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

import Control.Monad
import Control.Monad.Except