diff --git a/docs/coalton-lisp-interop.md b/docs/coalton-lisp-interop.md
index 05e71c85..1aada90a 100644
--- a/docs/coalton-lisp-interop.md
+++ b/docs/coalton-lisp-interop.md
@@ -196,17 +196,17 @@ There are two ways to call Coalton from Lisp.
 The safe way to call Coalton is to use the `coalton` operator. This will type check, compile, and evaluate a Coalton expression and return its value to Lisp. Note that `coalton` does not accept definitions or top-level forms. For example:
 
 ```lisp
-CL-USER> (format t "~R" (coalton:coalton coalton-library::(length (cons 1 (cons 2 nil)))))
+CL-USER> (format t "~R" (coalton:coalton (coalton-prelude:length (coalton:cons 1 (coalton:cons 2 coalton:nil)))))
 two     ; <- printed output
 NIL     ; <- returned value
-CL-USER> (format t "~R" (coalton:coalton coalton-library::(length 1)))
+CL-USER> (format t "~R" (coalton:coalton (coalton-prelude:length (coalton:the coalton:UFix 1))))
 ; (Guaranteed Compile-Time Error:)
-;
-; Failed to unify types COALTON:INTEGER 
-;                   and (COALTON-LIBRARY:LIST :B)
-; in unification of types (COALTON:INTEGER → :A)
-;                     and ((COALTON-LIBRARY:LIST :B) → COALTON:INTEGER)
-; in COALTON
+; error: Type mismatch
+;   --> repl input:1:46
+;    |
+;  1 |  (COALTON:COALTON (COALTON-LIBRARY/LIST:LENGTH (COALTON:THE COALTON:UFIX 1)))
+;    |                                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Expected type '(COALTON:LIST #T53400)' but got 'COALTON:UFIX'
+;    [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
 ```
 
 ### Unsafe Calls
@@ -214,10 +214,10 @@ CL-USER> (format t "~R" (coalton:coalton coalton-library::(length 1)))
 Using the aforementioned promises, it's possible to call into raw Coalton-compiled code by using the generated functions. These calls are not checked in any way!
 
 ```lisp
-CL-USER> (format t "~R" coalton-library::(length (cons 1 (cons 2 nil))))
+CL-USER> (format t "~R" (coalton-prelude:length (coalton:cons 1 (coalton:cons 2 coalton:nil))))
 two     ; <- printed output
 NIL     ; <- returned value
-CL-USER> (format t "~R" coalton-library::(length 1))
+CL-USER> (format t "~R" (coalton-prelude:length 1))
 ; (Possible Run-Time Error #1:)
 ;
 ; The value
diff --git a/docs/intro-to-coalton.md b/docs/intro-to-coalton.md
index 3cb09647..f822b457 100644
--- a/docs/intro-to-coalton.md
+++ b/docs/intro-to-coalton.md
@@ -1,4 +1,4 @@
-# Whirlwind Tour of Coalton
+# Intro to Coalton
 
 Coalton is a statically typed language that is embedded in, and compiles to, Common Lisp.
 
@@ -491,16 +491,14 @@ COALTON-USER> (type-of '/)
 ∀ :A :B. DIVIDABLE :A :B ⇒ (:A → :A → :B)
 ```
 
-Because of the generic nature of division, if you're computing some values at the REPL, "raw division" simply does not work.
+Because of [Instance Defaulting](#instance-defaulting), division of `Integer` constants without any additional context defaults to `Double-Float` division:
 
 ```
 COALTON-USER> (coalton (/ 1 2))
-Failed to reduce context for DIVIDABLE INTEGER :A
-in COALTON
-   [Condition of type COALTON-IMPL/TYPECHECKER::COALTON-TYPE-ERROR-CONTEXT]
+0.5d0
 ```
 
-You have to constrain the result type of the `Dividable` instance. You can do this with the `the` operator. There are lots of `Dividable` instances made for you.
+We can inform Coalton that our constants are of another type by constraining them with `the` or relying on type inference. For example, in order to get a non-Double-Float result from `Integer` inputs, you have to constrain the result type to your desired type (as long as the type has a defined instance of the `Dividable` type class):
 
 ```
 COALTON-USER> (coalton (the Single-Float (/ 4 2)))
@@ -509,13 +507,17 @@ COALTON-USER> (coalton (the Fraction (/ 4 2)))
 #.(COALTON-LIBRARY::%FRACTION 2 1)
 ```
 
-But division of integers does not work.
+An `Integer` result from division with `/` is not possible, as the instance `Dividable Integer Integer` is not defined:
 
 ```
 COALTON-USER> (coalton (the Integer (/ 4 2)))
-Failed to reduce context for DIVIDABLE INTEGER :A
-in COALTON
-   [Condition of type COALTON-IMPL/TYPECHECKER::COALTON-TYPE-ERROR-CONTEXT]
+; error: Unable to codegen
+;   --> repl input:1:22
+;    |
+;  1 |  (COALTON (THE INTEGER (/ 4 2)))
+;    |                        ^^^^^^^ expression has type ∀. (RECIPROCABLE INTEGER) => INTEGER with unresolved constraint (RECIPROCABLE INTEGER)
+;    |                        ------- Add a type assertion with THE to resolve ambiguity
+;    [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
 ```
 
 Why shouldn't this just be `2`?! The unfortunate answer is because `/` might not *always* produce an integer `2`, and when it doesn't divide exactly, Coalton doesn't force a particular way of rounding. As such, the proper way to do it is divide exactly, then round as you please with `floor`, `ceiling`, or `round`.
@@ -561,13 +563,13 @@ Lists must be homogeneous. This means the following produces a type error.
 
 ```
 COALTON-USER> (coalton-toplevel
-                (define wut (make-list 1 2 3.0)))
-
-Failed to unify types SINGLE-FLOAT and INTEGER
-in unification of types (INTEGER → (LIST SINGLE-FLOAT) → :A) and (:B → (LIST :B) → (LIST :B))
-in definition of WUT
-in COALTON-TOPLEVEL
-   [Condition of type COALTON-IMPL/TYPECHECKER::COALTON-TYPE-ERROR-CONTEXT]
+                (define wut (make-list 1.0d0 2.0d0 3.0)))
+; error: Type mismatch
+;   --> repl input:3:4
+;    |
+;  3 |      (MAKE-LIST 1.0d0 2.0d0 3.0)))
+;    |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Expected type '(LIST DOUBLE-FLOAT)' but got '(LIST SINGLE-FLOAT)' 
+;    [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
 ```
 
 Lists can also be deconstructed with `match`.
@@ -587,14 +589,14 @@ Coalton code is statically typechecked. Types are inferred.
 ```lisp
 (coalton-toplevel
   (define (fun x)
-    (map (+ 2) (parse-int x))))
+    (map (+ 2) (string:parse-int x))))
 ```
 
 The type of a variable or function can be checked with `coalton:type-of`.
 
 ```
 COALTON-USER> (type-of 'fun)
-(STRING -> (OPTIONAL INT)
+(STRING -> (OPTIONAL INTEGER)
 ```
 
 Type declarations can always be added manually.
@@ -603,7 +605,7 @@ Type declarations can always be added manually.
 (coalton-toplevel
   (declare fun (String -> (Optional Integer)))
   (define (fun x)
-    (map (+ 2) (parse-int x))))
+    (map (+ 2) (string:parse-int x))))
 ```
 
 Type declarations can also be added in let expressions
@@ -684,13 +686,19 @@ The into method is used only when a conversion can always be performed from one
       ((Some (Some x_)) (Some x_))
       (_ None)))
 
-
-  ;; Literal values can also be matched on
+  ;; Integers or Strings can also be matched on
   (define (is-5-or-7 x)
     (match x
       (5 True)
       (7 True)
-      (_ False))))
+      (_ False)))
+      
+  (define (is-five-or-seven x)
+    (match x
+      ("five"  True)
+      ("seven" True)
+      (_       False))))
+    
 ```
 
 Functions can pattern match on their arguments, but the patterns must be exhaustive.