tchajed

#!/bin/sh

verus --log-smt example.rs
# output is in .verus-log/root.smt2

tchajed

#!/bin/sh

dafny verify --solver-log example.smt2 --boogie /normalizeNames:0 example.dfy

tchajed

#!/usr/bin/env bash

# iris-release.sh prepares a commit for https://github.com/coq/opam to
# add a new version of std++ and Iris to the Coq opam repository.
#
# Requires a clone of opam-coq-archive. The opam files from std++ and Iris are
# retrieved by downloading their releases by tag.

set -eu

tchajed

#!/bin/bash

info() {
  echo -e "\033[34m$1\033[0m"
}

error() {
  echo -e "\033[31m$1\033[0m"
}

tchajed

method sum_seq(xs: seq<int>) returns (z:int) {
    var sum := 0;
    var i := 0;
    while i < |xs|
        invariant i <= |xs|
    {
        sum := sum + xs[i];
        i := i + 1;
    }
    return sum;

tchajed

#!/bin/bash

# basic manual argument parsing

usage() {
  echo "Usage: $0 [--foo FOO] [-v]" 1>&2
}

foo=""
verbose=false

tchajed

let blacklists = ["https://mail.google.com/*", "https://docs.google.com/document/*]
let newtab = "https://www.google.com"

tchajed

Keybase proof

I hereby claim:

• I am tchajed on github.
• I am tchajed (https://keybase.io/tchajed) on keybase.
• I have a public key ASBxd3t8HGdTAbKbOqOp5jrcJk3pusQbgsd5umQdsV0NTgo

To claim this, I am signing this object:

tchajed

Definition Reader E T := E -> T.

Definition get {E} : Reader E E := fun e => e.

Definition pure {E T} (x:T) : Reader E T := fun _ => x.

Definition ap {E A B} (f: Reader E (A -> B)) : Reader E A -> Reader E B :=
  fun x => fun e => f e (x e).

Infix "<*>" := (ap) (at level 11, left associativity).

tchajed

# Fish users
# Save this file as ~/.config/fish/functions/man.fish

function man
env \
    LESS_TERMCAP_mb=\e"[1;31m" \
    LESS_TERMCAP_md=\e"[1;31m" \
    LESS_TERMCAP_me=\e"[0m" \
    LESS_TERMCAP_se=\e"[0m" \
    LESS_TERMCAP_so=\e"[1;44;33m" \