Jared Tobin jtobin

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

## NixOS-On-Linode.md

      
        
          
            
              
              1 file
            
          
          
            
              
              2 forks
            
          
          
            
              
              11 comments
            
          
          
            
              
              23 stars
            
          
        
        
          
              
          
          
            
                nocoolnametom
                / NixOS-On-Linode.md
            
            
              Last active
              January 28, 2023 17:42
            
          
        
      
        
  
      
    Installing on Linode

There are now official docs, so follow those as they'll be up-to-date and easier to follow.

Click here to view the old directions
Installing on Linode
	(* 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.