diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,8 @@
+* 0.1.1.0 (21 January 2022)
+
+  - `->`, `/\`, `\/` syntax for implies, and, or
+  - `truthtable.disco` example
+  - Coinductively check user-defined types for qualifiers (#317)
+  - Additional documentation
+
+* 0.1.0.0 (17 January 2022): initial release
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -20,7 +20,32 @@
   (if you don't know what that is, then you don't have it), see the
   [instructions here](https://www.haskell.org/ghcup/install/) for a
   PowerShell command to run.
+    - If you use PowerShell, note that after running the magic
+      PowerShell command to set up `ghcup`, you need to close and
+      reopen PowerShell in order for it to recognize the `cabal`
+      command.
+
+- Run `cabal update`, which will download the latest information about
+  Haskell packages.
+
 - Now run `cabal install disco` at a command prompt.
+
+    - Note that this may take a very long time, on the order of an
+      hour or so.
+    - The good news is that most of this work only needs to be done
+      once, even if you later install an updated version of disco.
+      Even if installation fails partway through, the work already
+      completed up to that point need not be redone.
+    - On OSX, if building fails with an error like `ghc: could not
+      execute: opt`, it means you need to install LLVM.  The easiest
+      way to do this is to first [follow the instructions to install
+      Homebrew](https://brew.sh/) (if you don't already have it), and
+      then type
+
+          brew install llvm
+
+      at a terminal prompt.
+
 - If it works, you should be able to now type `disco` at a command
   prompt, which should display a message like this:
 
@@ -31,6 +56,21 @@
 
     Disco>
     ```
+
+- If installation seems like it succeeded but the `disco` command is
+  not recognized, it may be an issue with your path environment
+  variable settings.  Try running `disco` using an explicit path:
+    - `~/.cabal/bin/disco` on Linux or OSX
+    - `C:\cabal\bin\disco` on Windows
+    - If those don't work, poke around and see if you can figure
+      out where the `cabal/bin` folder is on your computer, and
+      run `disco` from there.
+    - If you wish, you may add the `cabal/bin` folder (wherever it is
+      located) to your `Path` (Windows) or `PATH` (Linux/OSX)
+      environment variable, so that you can run disco simply by typing
+      `disco`.  However, this step is optional.
+
+
 
 If you encounter any difficulties, please let me know --- either come
 talk to me or [open a GitHub
diff --git a/disco.cabal b/disco.cabal
--- a/disco.cabal
+++ b/disco.cabal
@@ -1,6 +1,6 @@
 cabal-version:       2.4
 name:                disco
-version:             0.1.0.0
+version:             0.1.1.0
 synopsis:            Functional programming language for teaching discrete math.
 description:         Disco is a simple functional programming language for use in
                      teaching discrete math.  Its syntax is designed to be close
@@ -9,7 +9,7 @@
 license-file:        LICENSE
 author:              Disco team
 maintainer:          byorgey@gmail.com
-copyright:           Disco team 2016 (see LICENSE)
+copyright:           Disco team 2016-2022 (see LICENSE)
 category:            Language
 
 tested-with:         GHC == 8.10.4
@@ -18,7 +18,7 @@
 
 data-files:          *.disco
 
-extra-source-files:  README.md, stack.yaml, example/*.disco, repl/*.hs
+extra-source-files:  README.md, CHANGELOG.md, stack.yaml, example/*.disco, repl/*.hs
                      docs/tutorial/example/*.disco
                      --- TEST FILES BEGIN (updated automatically by add-test-files.hs) ---
                      test/README.md
diff --git a/example/truthtable.disco b/example/truthtable.disco
new file mode 100644
--- /dev/null
+++ b/example/truthtable.disco
@@ -0,0 +1,19 @@
+import string
+
+||| Print a truth table for a binary boolean operation.  Intended to be used with
+||| the :print command, as in
+|||
+|||   :print truthtable(~/\~)
+!!! truthtable(~/\~) == "| F | F | F |\n| F | T | F |\n| T | F | F |\n| T | T | T |"
+truthtable : (Bool * Bool -> Bool) -> List(Char)
+truthtable(op) =
+  unlines [ fmtrow [x,y,op(x,y)] | x <- enumerate(Bool), y <- enumerate(Bool) ]
+
+||| Format a row of Boolean values with intervening | characters.
+!!! fmtrow [true, false, false, true] == "| T | F | F | T |"
+fmtrow : List(Bool) -> List(Char)
+fmtrow(bs) = append("|", concat([ append(fmtbool(b), " |") | b <- bs ]))
+
+fmtbool : Bool -> List(Char)
+fmtbool(true) = " T"
+fmtbool(false) = " F"
diff --git a/lib/string.disco b/lib/string.disco
new file mode 100644
--- /dev/null
+++ b/lib/string.disco
@@ -0,0 +1,7 @@
+-- type String = List(Char)
+
+unlines : List(List(Char)) -> List(Char)
+unlines([]) = []
+unlines([l]) = l
+unlines(l :: ls) = append(l, append("\n", unlines(ls)))
+
diff --git a/src/Disco/Error.hs b/src/Disco/Error.hs
--- a/src/Disco/Error.hs
+++ b/src/Disco/Error.hs
@@ -108,6 +108,9 @@
 rtd :: String -> Sem r Doc
 rtd page = "https://disco-lang.readthedocs.io/en/latest/reference/" <> text page <> ".html"
 
+issue :: Int -> Sem r Doc
+issue n = "See https://github.com/disco-lang/disco/issues/" <> text (show n)
+
 cyclicImportError
   :: Members '[Reader PA, LFresh] r
   => [ModuleName] -> Sem r Doc
diff --git a/src/Disco/Interactive/Commands.hs b/src/Disco/Interactive/Commands.hs
--- a/src/Disco/Interactive/Commands.hs
+++ b/src/Disco/Interactive/Commands.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE PatternSynonyms    #-}
 {-# LANGUAGE StandaloneDeriving #-}
 
 -----------------------------------------------------------------------------
@@ -71,7 +72,7 @@
                                                    toPrim)
 import           Disco.Typecheck
 import           Disco.Typecheck.Erase
-import           Disco.Types                      (toPolyType)
+import           Disco.Types                      (pattern TyString, toPolyType)
 import           Disco.Value
 
 ------------------------------------------------------------
@@ -87,6 +88,7 @@
   ShowDefn  :: Name Term -> REPLExpr 'CShowDefn  -- Show a variable's definition
   Parse     :: Term      -> REPLExpr 'CParse     -- Show the parsed AST
   Pretty    :: Term      -> REPLExpr 'CPretty    -- Pretty-print a term
+  Print     :: Term      -> REPLExpr 'CPrint     -- Print a string
   Ann       :: Term      -> REPLExpr 'CAnn       -- Show type-annotated term
   Desugar   :: Term      -> REPLExpr 'CDesugar   -- Show a desugared term
   Compile   :: Term      -> REPLExpr 'CCompile   -- Show a compiled term
@@ -130,6 +132,7 @@
   | CShowDefn
   | CParse
   | CPretty
+  | CPrint
   | CAnn
   | CDesugar
   | CCompile
@@ -208,6 +211,7 @@
     SomeCmd nopCmd,
     SomeCmd parseCmd,
     SomeCmd prettyCmd,
+    SomeCmd printCmd,
     SomeCmd reloadCmd,
     SomeCmd showDefnCmd,
     SomeCmd typeCheckCmd,
@@ -441,16 +445,17 @@
 handleEval (Eval m) = do
   mi <- inputToState @TopInfo $ loadParsedDiscoModule False FromCwdOrStdlib REPLModule m
   addToREPLModule mi
-  forM_ (mi ^. miTerms) (mapError EvalErr . evalTerm . fst)
+  forM_ (mi ^. miTerms) (mapError EvalErr . evalTerm True . fst)
   -- garbageCollect?
 
-evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => ATerm -> Sem r Value
-evalTerm at = do
+-- First argument = should the value be printed?
+evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => Bool -> ATerm -> Sem r Value
+evalTerm pr at = do
   env <- use @TopInfo topEnv
   v <- runInputConst env $ eval (compileTerm at)
 
   tydefs <- use @TopInfo (replModInfo . to allTydefs)
-  info $ runInputConst tydefs $ prettyValue' ty v
+  when pr $ info $ runInputConst tydefs $ prettyValue' ty v
 
   modify @TopInfo $
     (replModInfo . miTys %~ Ctx.insert (QName (QualifiedName REPLModule) (string2Name "it")) (toPolyType ty)) .
@@ -655,6 +660,31 @@
 
 handlePretty :: Members '[LFresh, Output Message] r => REPLExpr 'CPretty -> Sem r ()
 handlePretty (Pretty t) = info $ pretty' t
+
+------------------------------------------------------------
+-- :print
+
+printCmd :: REPLCommand 'CPrint
+printCmd =
+  REPLCommand
+    { name = "print",
+      helpcmd = ":print <expr>",
+      shortHelp = "Print a string without the double quotes, interpreting special characters",
+      category = User,
+      cmdtype = ColonCmd,
+      action = \x -> handlePrint x,
+      parser = Print <$> term
+    }
+
+handlePrint :: Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CPrint -> Sem r ()
+handlePrint (Print t) = do
+  (at, _) <- inputToState . typecheckTop $ inferTop t
+  let ty = getType at
+  case ty of
+    TyString -> do
+      v <- mapError EvalErr . evalTerm False $ at
+      info $ text (vlist vchar v)
+    _        -> err $ "Argument to :print must have type List(Char), not" <+> pretty' ty
 
 ------------------------------------------------------------
 -- :reload
diff --git a/src/Disco/Syntax/Operators.hs b/src/Disco/Syntax/Operators.hs
--- a/src/Disco/Syntax/Operators.hs
+++ b/src/Disco/Syntax/Operators.hs
@@ -165,11 +165,11 @@
     , bopInfo InL  Subset  ["subset", "⊆"]
     , bopInfo InL  Elem    ["elem", "∈"]
     ]
-  , [ bopInfo InR  And     ["and", "∧", "&&"]
+  , [ bopInfo InR  And     ["/\\", "and", "∧", "&&"]
     ]
-  , [ bopInfo InR  Or      ["or", "∨", "||"]
+  , [ bopInfo InR  Or      ["\\/", "or", "∨", "||"]
     ]
-  , [ bopInfo InR Impl     ["==>", "implies"]
+  , [ bopInfo InR Impl     ["->", "==>", "implies"]
     ]
   ]
   where
diff --git a/src/Disco/Syntax/Prims.hs b/src/Disco/Syntax/Prims.hs
--- a/src/Disco/Syntax/Prims.hs
+++ b/src/Disco/Syntax/Prims.hs
@@ -195,10 +195,10 @@
   , PrimFloor    ==> "floor(x) is the largest integer which is <= x."
   , PrimCeil     ==> "ceiling(x) is the smallest integer which is >= x."
   , PrimAbs      ==> "abs(x) is the absolute value of x.  Also written |x|."
-  , PrimUOp Not  ==> "Logical negation: ¬true = false and ¬false = true.  Also written 'not'."
-  , PrimBOp And  ==> "Logical conjunction (and): true and true = true; otherwise x and y = false."
-  , PrimBOp Or   ==> "Logical disjunction (or): false or false = false; otherwise x or y = true."
-  , PrimBOp Impl ==> "Logical implication (implies): true ==> false = false; otherwise x ==> y = true."
+  , PrimUOp Not  ==> "Logical negation: not(true) = false and not(false) = true."
+  , PrimBOp And  ==> "Logical conjunction (and): true /\\ true = true; otherwise x /\\ y = false."
+  , PrimBOp Or   ==> "Logical disjunction (or): false \\/ false = false; otherwise x \\/ y = true."
+  , PrimBOp Impl ==> "Logical implication (implies): true -> false = false; otherwise x -> y = true."
   , PrimBOp Eq   ==> "Equality test.  x == y is true if x and y are equal."
   , PrimBOp Neq  ==> "Inequality test.  x /= y is true if x and y are unequal."
   , PrimBOp Lt   ==> "Less-than test. x < y is true if x is less than (but not equal to) y."
@@ -225,5 +225,8 @@
   , PrimFloor    ==> "round"
   , PrimCeil     ==> "round"
   , PrimAbs      ==> "abs"
-  , PrimUOp Not  ==> "not"
+  , PrimUOp Not  ==> "logic-ops"
+  , PrimBOp And  ==> "logic-ops"
+  , PrimBOp Or   ==> "logic-ops"
+  , PrimBOp Impl ==> "logic-ops"
   ]
diff --git a/src/Disco/Typecheck/Solve.hs b/src/Disco/Typecheck/Solve.hs
--- a/src/Disco/Typecheck/Solve.hs
+++ b/src/Disco/Typecheck/Solve.hs
@@ -43,6 +43,7 @@
 import           Disco.Effects.State
 import           Polysemy
 import           Polysemy.Error
+import           Polysemy.Input
 import           Polysemy.Output
 
 import           Disco.Messages
@@ -230,9 +231,9 @@
 -- Top-level solver algorithm
 
 solveConstraint
-  :: Members '[Fresh, Error SolveError, Output Message] r
-  => TyDefCtx -> Constraint -> Sem r S
-solveConstraint tyDefns c = do
+  :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r
+  => Constraint -> Sem r S
+solveConstraint c = do
 
   -- Step 1. Open foralls (instantiating with skolem variables) and
   -- collect wanted qualifiers; also expand disjunctions.  Result in a
@@ -249,16 +250,18 @@
 
   -- Now try continuing with each set and pick the first one that has
   -- a solution.
-  asum' (map (uncurry (solveConstraintChoice tyDefns)) qcList)
+  asum' (map (uncurry solveConstraintChoice) qcList)
 
 solveConstraintChoice
-  :: Members '[Fresh, Error SolveError, Output Message] r
-  => TyDefCtx -> TyVarInfoMap -> [SimpleConstraint] -> Sem r S
-solveConstraintChoice tyDefns quals cs = do
+  :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r
+  => TyVarInfoMap -> [SimpleConstraint] -> Sem r S
+solveConstraintChoice quals cs = do
 
   debugPretty quals
   debug $ vcat (map pretty' cs)
 
+  tyDefns <- input @TyDefCtx
+
   -- Step 2. Check for weak unification to ensure termination. (a la
   -- Traytel et al).
 
@@ -273,7 +276,7 @@
   debug "------------------------------"
   debug "Running simplifier..."
 
-  (vm, atoms, theta_simp) <- simplify tyDefns quals cs
+  (vm, atoms, theta_simp) <- simplify quals cs
   debug "Done running simplifier. Results:"
 
   debugPretty vm
@@ -306,7 +309,7 @@
   debug "------------------------------"
   debug "Checking WCCs for skolems..."
 
-  (g', theta_skolem) <- checkSkolems tyDefns vm g
+  (g', theta_skolem) <- checkSkolems vm g
   debugPretty theta_skolem
 
   -- We don't need to ensure that theta_skolem respects sorts since
@@ -372,7 +375,7 @@
 -- Step 1. Constraint decomposition.
 
 decomposeConstraint
-  :: Members '[Fresh, Error SolveError] r
+  :: Members '[Fresh, Error SolveError, Input TyDefCtx] r
   => Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
 decomposeConstraint (CSub t1 t2) = return [(mempty, [t1 :<: t2])]
 decomposeConstraint (CEq  t1 t2) = return [(mempty, [t1 :=: t2])]
@@ -391,16 +394,37 @@
 decomposeConstraint (COr cs)     = concat <$> filterErrors (map decomposeConstraint cs)
 
 decomposeQual
-  :: Members '[Fresh, Error SolveError] r
+  :: Members '[Fresh, Error SolveError, Input TyDefCtx] r
   => Type -> Qualifier -> Sem r TyVarInfoMap
-decomposeQual (TyAtom a) q             = checkQual q a
-  -- XXX Really we should be able to check by induction whether a
-  -- user-defined type has a certain sort.
-decomposeQual ty@(TyCon (CUser _) _) q = throw $ Unqual q ty
-decomposeQual ty@(TyCon c tys) q
-  = case qualRules c q of
+decomposeQual = go S.empty
+  where
+    go :: Members '[Fresh, Error SolveError, Input TyDefCtx] r
+       => Set (String, [Type], Qualifier) -> Type -> Qualifier -> Sem r TyVarInfoMap
+
+    -- For a type atom, call out to checkQual.
+    go _ (TyAtom a) q = checkQual q a
+
+    -- Coinductively check user-defined types for a qualifier.  Keep
+    -- track of a set of user-defined types and qualifiers we have
+    -- seen.  Every time we encounter a new one, add it to the set and
+    -- recurse on its unfolding.  If we ever encounter one we have
+    -- already seen, we can assume by coinduction that the qualifier
+    -- is satisfied.
+    go seen (TyCon (CUser t) tys) q = do
+      case (t, tys, q) `S.member` seen of
+        True -> return mempty
+        False -> do
+          tyDefns <- input @TyDefCtx
+          case M.lookup t tyDefns of
+            Nothing  -> error $ show t ++ " not in ty defn map!!"
+            Just (TyDefBody _ body) -> do
+              let ty' = body tys
+              go (S.insert (t, tys, q) seen) ty' q
+
+    -- Otherwise, decompose a type constructor according to the qualRules.
+    go seen ty@(TyCon c tys) q = case qualRules c q of
       Nothing -> throw $ Unqual q ty
-      Just qs -> mconcat <$> zipWithM (maybe (return mempty) . decomposeQual) tys qs
+      Just qs -> mconcat <$> zipWithM (maybe (return mempty) . go seen) tys qs
 
 checkQual
   :: Members '[Fresh, Error SolveError] r
@@ -427,9 +451,9 @@
 --   (b <: v), where v is a type variable and b is a base type.
 
 simplify
-  :: Members '[Error SolveError, Output Message] r
-  => TyDefCtx -> TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
-simplify tyDefns origVM cs
+  :: Members '[Error SolveError, Output Message, Input TyDefCtx] r
+  => TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
+simplify origVM cs
   = (\(SS vm' cs' s' _) -> (vm', map extractAtoms cs', s'))
   -- contFreshMT :: Monad m => FreshMT m a -> Integer -> m a
   -- "Run a FreshMT computation given a starting index for fresh name generation."
@@ -456,7 +480,7 @@
     -- Iterate picking one simplifiable constraint and simplifying it
     -- until none are left.
     simplify'
-      :: Members '[State SimplifyState, Fresh, Error SolveError, Output Message] r
+      :: Members '[State SimplifyState, Fresh, Error SolveError, Output Message, Input TyDefCtx] r
       => Sem r ()
     simplify' = do
       -- q <- gets fst
@@ -517,7 +541,7 @@
     -- has already been seen before (due to expansion of a recursive
     -- type), just throw it away and stop.
     simplifyOne
-      :: Members '[State SimplifyState, Fresh, Error SolveError] r
+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
       => SimpleConstraint -> Sem r ()
     simplifyOne c = do
       seen <- use ssSeen
@@ -528,14 +552,15 @@
           simplifyOne' c
 
     simplifyOne'
-      :: Members '[State SimplifyState, Fresh, Error SolveError] r
+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
       => SimpleConstraint -> Sem r ()
 
     -- If we have an equality constraint, run unification on it.  The
     -- resulting substitution is applied to the remaining constraints
     -- as well as prepended to the current substitution.
 
-    simplifyOne' (ty1 :=: ty2) =
+    simplifyOne' (ty1 :=: ty2) = do
+      tyDefns <- input @TyDefCtx
       case unify tyDefns [(ty1, ty2)] of
         Nothing -> throw NoUnify
         Just s' -> extendSubst s'
@@ -549,7 +574,8 @@
       = simplifyOne' (ty1 :=: ty2)
 
     -- Otherwise, expand the user-defined type and continue.
-    simplifyOne' (TyCon (CUser t) ts :<: ty2) =
+    simplifyOne' (TyCon (CUser t) ts :<: ty2) = do
+      tyDefns <- input @TyDefCtx
       case M.lookup t tyDefns of
         Nothing  -> error $ show t ++ " not in ty defn map!"
         Just (TyDefBody _ body) ->
@@ -559,7 +585,8 @@
     simplifyOne' (ty1@TyVar{} :<: ty2@(TyCon (CUser _) _))
       = simplifyOne' (ty1 :=: ty2)
 
-    simplifyOne' (ty1 :<: TyCon (CUser t) ts) =
+    simplifyOne' (ty1 :<: TyCon (CUser t) ts) = do
+      tyDefns <- input @TyDefCtx
       case M.lookup t tyDefns of
         Nothing  -> error $ show t ++ " not in ty defn map!"
         Just (TyDefBody _ body) ->
@@ -604,7 +631,7 @@
       error $ "Impossible! simplifyOne' " ++ show s ++ " :<: " ++ show t
 
     expandStruct
-      :: Members '[State SimplifyState, Fresh, Error SolveError] r
+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
       => Name Type -> Con -> SimpleConstraint -> Sem r ()
     expandStruct a c con = do
       as <- mapM (const (TyVar <$> fresh (string2Name "a"))) (arity c)
@@ -616,7 +643,7 @@
     -- 2. apply s' to constraints
     -- 3. apply s' to qualifier map and decompose
     extendSubst
-      :: Members '[State SimplifyState, Fresh, Error SolveError] r
+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
       => S -> Sem r ()
     extendSubst s' = do
       ssSubst %= (s'@@)
@@ -624,7 +651,7 @@
       substVarMap s'
 
     substVarMap
-      :: Members '[State SimplifyState, Fresh, Error SolveError] r
+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
       => S -> Sem r ()
     substVarMap s' = do
       vm <- use ssVarMap
@@ -688,9 +715,9 @@
 --   only unsorted variables, just unify them all with the skolem and
 --   remove those components.
 checkSkolems
-  :: Members '[Error SolveError, Output Message] r
-  => TyDefCtx -> TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
-checkSkolems tyDefns vm graph = do
+  :: Members '[Error SolveError, Output Message, Input TyDefCtx] r
+  => TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
+checkSkolems vm graph = do
   let skolemWCCs :: [Set Atom]
       skolemWCCs = filter (any isSkolem) $ G.wcc graph
 
@@ -715,9 +742,14 @@
     noSkolems (AVar (U v)) = UV v
     noSkolems (AVar (S v)) = error $ "Skolem " ++ show v ++ " remaining in noSkolems"
 
+    unifyWCCs
+      :: Members '[Error SolveError, Output Message, Input TyDefCtx] r
+      => Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
     unifyWCCs g s []     = return (G.map noSkolems g, s)
     unifyWCCs g s (u:us) = do
       debug $ "Unifying" <+> pretty' (u:us) <> "..."
+
+      tyDefns <- input @TyDefCtx
 
       let g' = foldl' (flip G.delete) g u
 
diff --git a/src/Disco/Typecheck/Util.hs b/src/Disco/Typecheck/Util.hs
--- a/src/Disco/Typecheck/Util.hs
+++ b/src/Disco/Typecheck/Util.hs
@@ -113,8 +113,7 @@
   => Sem (Writer Constraint ': r) a -> Sem r (a, S)
 solve m = do
   (a, c) <- withConstraint m
-  tds <- ask @TyDefCtx
-  res <- runSolve . solveConstraint tds $ c
+  res <- runSolve . inputToReader . solveConstraint $ c
   case res of
     Left e  -> throw (Unsolvable e)
     Right s -> return (a, s)
diff --git a/src/Disco/Types.hs b/src/Disco/Types.hs
--- a/src/Disco/Types.hs
+++ b/src/Disco/Types.hs
@@ -667,6 +667,8 @@
 
 -- XXX coinductively check whether user-defined types are searchable
 --   e.g.  L = Unit + N * L  ought to be searchable.
+--   See https://github.com/disco-lang/disco/issues/318.
+
 -- | Decide whether a type is searchable, i.e. effectively enumerable.
 isSearchable :: Type -> Bool
 isSearchable TyProp         = False
diff --git a/test/logic-bools/expected b/test/logic-bools/expected
--- a/test/logic-bools/expected
+++ b/test/logic-bools/expected
@@ -7,12 +7,18 @@
 false
 false
 false
+false
 true
 true
 true
 false
 true
+true
 false
+true
+true
+false
+true
 true
 true
 false
diff --git a/test/logic-bools/input b/test/logic-bools/input
--- a/test/logic-bools/input
+++ b/test/logic-bools/input
@@ -7,14 +7,20 @@
 false and true
 false and false
 true && false
+true /\ false
 true or true
 true or false
 false or true
 false or false
 true || false
+true \/ false
 not true
 not false
-true ==> true 
-true ==> false 
-false ==> true 
-false ==> false 
+true ==> true
+true ==> false
+false ==> true
+false ==> false
+true -> true
+true -> false
+false -> true
+false -> false
diff --git a/test/repl-doc/expected b/test/repl-doc/expected
--- a/test/repl-doc/expected
+++ b/test/repl-doc/expected
@@ -30,7 +30,7 @@
 Alternative syntax: ¬~
 precedence level 15
 
-Logical negation: ¬true = false and ¬false = true.  Also written 'not'.
+Logical negation: not(true) = false and not(false) = true.
 
 https://disco-lang.readthedocs.io/en/latest/reference/not.html
 
diff --git a/test/repl-help/expected b/test/repl-help/expected
--- a/test/repl-help/expected
+++ b/test/repl-help/expected
@@ -6,6 +6,7 @@
 :help             Show help
 :load <filename>  Load a file
 :names            Show all names in current scope
+:print <expr>     Print a string without the double quotes, interpreting special characters
 :reload           Reloads the most recently loaded file
 :test <property>  Test a property using random examples
 
diff --git a/test/repl-proptest/expected b/test/repl-proptest/expected
--- a/test/repl-proptest/expected
+++ b/test/repl-proptest/expected
@@ -1,10 +1,10 @@
   - Test passed: not false
   - Test passed: {1, 2} =!= {2, 1}
-  - Test passed: ∃a, b. (a and b) =!= (a or b)
+  - Test passed: ∃a, b. (a /\ b) =!= (a \/ b)
     Found example:
       a = false
       b = false
-  - Test result mismatch for: ∀a, b. (a and b) =!= (a or b)
+  - Test result mismatch for: ∀a, b. (a /\ b) =!= (a \/ b)
     - Left side:  true
     - Right side: false
     Counterexample:
diff --git a/test/types-standalone-ops/expected b/test/types-standalone-ops/expected
--- a/test/types-standalone-ops/expected
+++ b/test/types-standalone-ops/expected
@@ -1,4 +1,4 @@
-~and~ : Bool × Bool → Bool
-false and true : Bool
-λx. x and true : Bool → Bool
-let f : (Bool × Bool → Bool) → Bool = λg. g(true, false) in f(~and~) : Bool
+~/\~ : Bool × Bool → Bool
+false /\ true : Bool
+λx. x /\ true : Bool → Bool
+let f : (Bool × Bool → Bool) → Bool = λg. g(true, false) in f(~/\~) : Bool