tchajed

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

#!/bin/bash

# basic manual argument parsing

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

foo=""
verbose=false

tchajed

#!/bin/sh

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

tchajed

#!/bin/sh

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

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