Skip to content

Instantly share code, notes, and snippets.

Tej Chajed tchajed

Block or report user

Report or block tchajed

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
tchajed / iteration.dfy
Created Oct 15, 2019
Iterating over sequences and sets in Dafny
View iteration.dfy
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 /
Created Sep 21, 2019
Starting a bash script
set -e
blue=$(tput setaf 4)
green=$(tput setaf 2)
red=$(tput setaf 1)
reset=$(tput sgr0)
info() {
View svimrc
let blacklists = ["*", "*]
let newtab = ""

Keybase proof

I hereby claim:

  • I am tchajed on github.
  • I am tchajed ( on keybase.
  • I have a public key ASBxd3t8HGdTAbKbOqOp5jrcJk3pusQbgsd5umQdsV0NTgo

To claim this, I am signing this object:

tchajed / RecordUpdater.v
Last active Jul 23, 2018
Small library for creating record updaters in Coq
View RecordUpdater.v
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 /
Last active Aug 19, 2016 — forked from supermarin/.env
Colored `man` pages on OS X
# Fish users
# Save this file as ~/.config/fish/functions/
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" \
tchajed /
Last active Aug 12, 2016
Python re examples
import re
# match requires the entire string to match, while search will
# find a partial match
assert re.match("\d+", "123")
assert not re.match("\d+", "hello 123")
assert"\d+", "123")
assert"\d+", "hello 123")
tchajed / lambda-calculus.hs
Last active Aug 27, 2015
Parsec parser for the untyped lambda calculus
View lambda-calculus.hs
import Text.ParserCombinators.Parsec
import System.Environment (getArgs)
import Safe
data Expr =
Var Name -- variable
| App Expr Expr -- application
| Lambda Name Expr -- lambda abstraction
tchajed /
Last active Aug 29, 2015
Parse a CSV file of coordinates in Python
import csv
""" Read a CSV file of points.
Assumes each line of the file is a CSV list of coordinates, which are parsed as
def read_coords(fname):
with open(fname, 'rb') as f:
points = []
View chrome_load.js
// ==UserScript==
// @name jQuery For Chrome (A Cross Browser Example)
// @namespace jQueryForChromeExample
// @include *
// @author Erik Vergobbi Vold
// @description This userscript is meant to be an example on how to use jQuery in a userscript on Google Chrome.
// ==/UserScript==
// a function that loads jQuery and calls a callback function when jQuery has finished loading
function addJQuery(callback) {
You can’t perform that action at this time.