jaykru

(defgeneric move (state))
(defgeneric energy (state))

(defun prob-accept (old new temp)
  (let ((e-old (energy old))
        (e-new (energy new)))
    (if (< e-new e-old)
        1
        (exp (/ (- (- e-new e-old))
                (max 0.000000001 temp))))))

jaykru

import tactic.omega
import tactic

inductive LTL (T: Type) : Type
| injp : (T -> Prop) -> LTL
| false : LTL
| true : LTL
| imp : LTL -> LTL -> LTL
| until : LTL -> LTL -> LTL
| next : LTL -> LTL.

jaykru

jaykru

#!/usr/bin/env python3
import torch
import torch.nn.functional as F
device = torch.device("cuda" if torch.cuda.is_available() else "cpu")

words = open('names.txt', 'r').read().splitlines()
chars = sorted(list(set(''.join(words))))
stoi = {s:i+1 for i,s in enumerate(chars)}
stoi['.'] = 0
itos = {i:s for s,i in stoi.items()}

jaykru

type alphabet
type regexp =
  | Empty (* empty string! *)
  | Atom of alphabet
  | Star of regexp
  | Concat of regexp * regexp
  | Union of regexp * regexp

let rec core = function
  | Star r -> core r

jaykru

### usage notes:
# the graphviz `dot` program on my machine didn't like the output for some reason. no time to investigate.
# instead use https://rsms.me/graphviz/
# if the diagrams are too vertically squished, try ranksep=k as a property on the generated digraph

from gvgen import *
import more_itertools

two = [1,2]
three = [1,2,3]

jaykru

acpi
agda
bc
bogofilter
cmatrix
coq
coreutils
diffutils
dmenu
emacs

jaykru

Definition time := nat.
Section Theft.
  Context (Person Object: Set).

  (* In this meme we model monopolistic ownership of objects as follows:

     A person owns /with monopoly/ an object at time t if
     they were consensually given the object by someone who owned the object at time t-1.

     Retainment of an object over time is modeled as reflexive giving. *)

jaykru

with import ~/nixpkgs {
  crossSystem = (import ~/nixpkgs {}).lib.systems.examples.riscv64-embedded; # TODO: do this in a less clunky way?
};

mkShell {
  RISCV_PREFIX = "riscv64-none-elf-";
  stdenv = multiStdenv; # multilib compilers?
  buildInputs = [];
}

jaykru

### Keybase proof

I hereby claim:

  * I am jaykru on github.
  * I am jaykru (https://keybase.io/jaykru) on keybase.
  * I have a public key whose fingerprint is 26E4 EFBD 7E46 D915 444C  79D7 8EA8 679E BE63 8186

To claim this, I am signing this object: