Skip to content

Instantly share code, notes, and snippets.

Jared Tobin jtobin

Block or report user

Report or block jtobin

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
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

@andrejbauer
andrejbauer / topology.v
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.