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:
#!/bin/sh | |
verus --log-smt example.rs | |
# output is in .verus-log/root.smt2 |
#!/bin/sh | |
dafny verify --solver-log example.smt2 --boogie /normalizeNames:0 example.dfy |
#!/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 |
#!/bin/bash | |
info() { | |
echo -e "\033[34m$1\033[0m" | |
} | |
error() { | |
echo -e "\033[31m$1\033[0m" | |
} |
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; |
#!/bin/bash | |
# basic manual argument parsing | |
usage() { | |
echo "Usage: $0 [--foo FOO] [-v]" 1>&2 | |
} | |
foo="" | |
verbose=false |
let blacklists = ["https://mail.google.com/*", "https://docs.google.com/document/*] | |
let newtab = "https://www.google.com" |
I hereby claim:
To claim this, I am signing this object:
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). |
# 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" \ |