If your Mac is out-of-order or you otherwise cannot download macOS from the App Store, you can still create a bootable OS X recovery USB, and you can use that to create an Installer USB.
The downloads used in this process are legal and freely avaliable - including disk images directly from Apple's IT support pages, and open source utilities for extracting and converting pkg, dmg, and HFS+.
| #!/usr/bin/env bash | |
| set -eux | |
| # common functions | |
| function check_installed { | |
| if ! command -v "$1" &>/dev/null; then | |
| echo "Please install $1" | |
| exit 1 |
| data Tree : Nat -> Type where | |
| Leaf : Tree Z | |
| Branch : Nat -> Tree n -> Tree n -> Tree (S n) | |
| %name Tree lt, rt, t | |
| treeHeight : Tree n -> Nat | |
| treeHeight Leaf = 0 | |
| treeHeight (Branch k lt rt) = 1 + treeHeight lt | |
| treeHeightCheck : (t : Tree n) -> treeHeight t = n |
