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
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
tchajed / bash.sh
Created Sep 21, 2019
Starting a bash script
View bash.sh
#!/bin/bash
set -e
blue=$(tput setaf 4)
green=$(tput setaf 2)
red=$(tput setaf 1)
reset=$(tput sgr0)
info() {
View svimrc
let blacklists = ["https://mail.google.com/*", "https://docs.google.com/document/*]
let newtab = "https://www.google.com"
View keybase.md

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
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
tchajed / man.fish
Last active Aug 19, 2016 — forked from supermarin/.env
Colored `man` pages on OS X
View man.fish
# 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" \
@tchajed
tchajed / basic-re.py
Last active Aug 12, 2016
Python re examples
View basic-re.py
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 re.search("\d+", "123")
assert re.search("\d+", "hello 123")
@tchajed
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
deriving
(Eq,Show)
@tchajed
tchajed / coords.py
Last active Aug 29, 2015
Parse a CSV file of coordinates in Python
View coords.py
import csv
""" Read a CSV file of points.
Assumes each line of the file is a CSV list of coordinates, which are parsed as
floats.
"""
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.