Instantly share code, notes, and snippets.

# Jared Tobinjtobin

• Sort options
Last active Dec 28, 2019
View NixOS-On-Linode.md

# Installing on Linode

I copied the bulk of this guide from Andrew Miller's NixOS-On-Linode.md instructions. It's a very well-written guide, but I felt we could make things a bit more simple than he left them in his original guide.

This tutorial is written for people who want to run NixOS on a Linode instance. The installation is pretty straightforward, but it involves some bootstrapping using Linode's tools.

In this tutorial, we will show you how to set up NixOS on Linode by setting up disks (including the installation live CD) using the rescue OS, and use the minimal live CD to install NixOS onto your disk.

## Create a Linode

Last active Oct 22, 2019
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
View topology.v
 (* How do to topology in Coq if you are secretly an HOL fan. We will not use type classes or canonical structures because they count as "advanced" technology. But we will use notations. *) (* We think of subsets as propositional functions. Thus, if [A] is a type [x : A] and [U] is a subset of [A], [U x] means "[x] is an element of [U]". *) Definition P (A : Type) := A -> Prop.
You can’t perform that action at this time.