diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs
index 037e0667..aad84445 100644
--- a/cryptol-remote-api/cryptol-eval-server/Main.hs
+++ b/cryptol-remote-api/cryptol-eval-server/Main.hs
@@ -36,6 +36,8 @@ import qualified Argo.Doc as Doc
 import CryptolServer
     ( ServerState, moduleEnv, tcSolver, initialState, extendSearchPath, command, notification )
 import CryptolServer.Call ( call )
+import CryptolServer.Data.Expression ( Expression )
+import CryptolServer.Data.Type ( JSONSchema )
 import CryptolServer.EvalExpr
     ( evalExpressionDescr, evalExpression )
 import CryptolServer.ExtendSearchPath
@@ -90,7 +92,11 @@ evalServerDocs =
   [ Doc.Section "Summary" $ [ Doc.Paragraph
     [Doc.Text "A remote server for ",
      Doc.Link (Doc.URL "https://https://cryptol.net/") "Cryptol",
-     Doc.Text " that supports only type checking and evaluation of Cryptol code."]]]
+     Doc.Text " that supports only type checking and evaluation of Cryptol code."]]
+  , Doc.Section "Terms and Types"
+    [Doc.datatype @Expression,
+     Doc.datatype @JSONSchema]
+  ]
 
 description :: String
 description =
diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs
index c681f67b..50df6f28 100644
--- a/cryptol-remote-api/cryptol-remote-api/Main.hs
+++ b/cryptol-remote-api/cryptol-remote-api/Main.hs
@@ -18,6 +18,8 @@ import CryptolServer.Call ( call, callDescr )
 import CryptolServer.Check ( check, checkDescr )
 import CryptolServer.ClearState
     ( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr )
+import CryptolServer.Data.Expression ( Expression )
+import CryptolServer.Data.Type ( JSONSchema )
 import CryptolServer.EvalExpr
     ( evalExpression, evalExpressionDescr )
 import CryptolServer.ExtendSearchPath
@@ -47,7 +49,11 @@ serverDocs =
   [ Doc.Section "Summary" $ [ Doc.Paragraph
     [Doc.Text "An RCP server for ",
      Doc.Link (Doc.URL "https://https://cryptol.net/") "Cryptol",
-     Doc.Text " that supports type checking and evaluation of Cryptol code via the methods documented below."]]]
+     Doc.Text " that supports type checking and evaluation of Cryptol code via the methods documented below."]]
+  , Doc.Section "Terms and Types"
+    [Doc.datatype @Expression,
+     Doc.datatype @JSONSchema]
+  ]
 
 description :: String
 description =
diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs
index 05146204..59f5ffde 100644
--- a/cryptol-remote-api/src/CryptolServer.hs
+++ b/cryptol-remote-api/src/CryptolServer.hs
@@ -36,7 +36,7 @@ newtype CryptolNotification a = CryptolNotification { runCryptolNotification ::
 
 command ::
   forall params result.
-  (JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedParams params) =>
+  (JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedMethod params result) =>
   Text ->
   Doc.Block ->
   (params -> CryptolCommand result) ->
@@ -47,7 +47,7 @@ command name doc f = Argo.command name doc f'
 
 notification ::
   forall params.
-  (JSON.FromJSON params, Doc.DescribedParams params) =>
+  (JSON.FromJSON params, Doc.DescribedMethod params ()) =>
   Text ->
   Doc.Block ->
   (params -> CryptolNotification ()) ->
diff --git a/cryptol-remote-api/src/CryptolServer/Call.hs b/cryptol-remote-api/src/CryptolServer/Call.hs
index 05826968..2b0b11f4 100644
--- a/cryptol-remote-api/src/CryptolServer/Call.hs
+++ b/cryptol-remote-api/src/CryptolServer/Call.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ViewPatterns #-}
 module CryptolServer.Call
   ( Expression(..)
@@ -16,9 +18,11 @@ module CryptolServer.Call
 import qualified Argo.Doc as Doc
 import Data.Aeson as JSON hiding (Encoding, Value, decode)
 import qualified Data.Aeson as JSON
+import Data.Typeable (Proxy(..), typeRep)
 
 import CryptolServer
 import CryptolServer.Data.Expression
+import CryptolServer.Data.Type
 import CryptolServer.EvalExpr (evalExpression')
 
 callDescr :: Doc.Block
@@ -42,10 +46,25 @@ instance FromJSON CallParams where
     withObject "params for \"call\"" $
     \o -> CallParams <$> o .: "function" <*> o .: "arguments"
 
-instance Doc.DescribedParams CallParams where
+instance Doc.DescribedMethod CallParams JSON.Value where
   parameterFieldDescription =
     [("function",
       Doc.Paragraph [Doc.Text "The function being called."])
     , ("arguments",
       Doc.Paragraph [Doc.Text "The arguments the function is being applied to."])
     ]
+
+  resultFieldDescription =
+    [ ("value",
+      Doc.Paragraph [ Doc.Text "A "
+                    , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
+                    , Doc.Text " that denotes the value"
+                    ])
+    , ("type",
+      Doc.Paragraph [ Doc.Text " A"
+                    , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type"
+                    , Doc.Text " that denotes the result type"
+                    ])
+    , ("type string",
+      Doc.Paragraph [Doc.Text "A human-readable representation of the result type"])
+    ]
diff --git a/cryptol-remote-api/src/CryptolServer/Check.hs b/cryptol-remote-api/src/CryptolServer/Check.hs
index 794956f1..ba76820d 100644
--- a/cryptol-remote-api/src/CryptolServer/Check.hs
+++ b/cryptol-remote-api/src/CryptolServer/Check.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -166,7 +167,7 @@ instance FromJSON CheckParams where
               Right n -> pure $ Just $ RandomCheckMode $ (toInteger :: Int -> Integer) n) v)
       num Nothing = pure Nothing
 
-instance Doc.DescribedParams CheckParams where
+instance Doc.DescribedMethod CheckParams CheckResult where
   parameterFieldDescription =
     [ ("expression",
       Doc.Paragraph [Doc.Text "The predicate (i.e., function) to check; "
@@ -182,3 +183,29 @@ instance Doc.DescribedParams CheckParams where
                     , Doc.Text " sufficiently small, checking may take longer than you are willing to wait!"
                       ])
     ]
+
+  resultFieldDescription =
+    [ ("tests run",
+      Doc.Paragraph [Doc.Text "The number of tests that were successfully run."])
+    , ("tests possible",
+      Doc.Paragraph [Doc.Text "The maximum number of possible tests."])
+    , ("result",
+      Doc.Paragraph [ Doc.Text "The overall test result, represented as one of three string values:"
+                    , Doc.Literal "pass", Doc.Text " (all tests succeeded), "
+                    , Doc.Literal "fail", Doc.Text " (a test evaluated to ", Doc.Literal "False", Doc.Text "), or"
+                    , Doc.Literal "error", Doc.Text " (an exception was raised during evaluation)."
+                    ])
+    , ("arguments",
+      Doc.Paragraph [ Doc.Text "Only returned if the ", Doc.Literal "result"
+                    , Doc.Text " is ", Doc.Literal "fail", Doc.Text " or ", Doc.Literal "error", Doc.Text ". "
+                    , Doc.Text "An array of JSON objects indicating the arguments passed to the property "
+                    , Doc.Text "which triggered the failure or error. Each object has an "
+                    , Doc.Literal "expr", Doc.Text " field, which is an individual argument expression, and a "
+                    , Doc.Literal "type", Doc.Text " field, which is the type of the argument expression."
+                    ])
+    , ("error message",
+      Doc.Paragraph [ Doc.Text "Only returned if the ", Doc.Literal "result"
+                    , Doc.Text " is ", Doc.Literal "error", Doc.Text ". "
+                    , Doc.Text "A human-readable representation of the exception that was raised during evaluation."
+                    ])
+    ]
diff --git a/cryptol-remote-api/src/CryptolServer/ClearState.hs b/cryptol-remote-api/src/CryptolServer/ClearState.hs
index efe18b9c..0eed3512 100644
--- a/cryptol-remote-api/src/CryptolServer/ClearState.hs
+++ b/cryptol-remote-api/src/CryptolServer/ClearState.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 module CryptolServer.ClearState
   ( clearState
@@ -20,8 +21,8 @@ instance JSON.FromJSON ClearStateParams where
     JSON.withObject "params for \"clear state\"" $
     \o -> ClearStateParams <$> o .: "state to clear"
 
-instance Doc.DescribedParams ClearStateParams where
-  parameterFieldDescription = 
+instance Doc.DescribedMethod ClearStateParams () where
+  parameterFieldDescription =
     [("state to clear",
        Doc.Paragraph [Doc.Text "The state to clear from the server to make room for other unrelated states."])
      ]
@@ -42,7 +43,7 @@ instance JSON.FromJSON ClearAllStatesParams where
     JSON.withObject "params for \"clear all states\"" $
     \_ -> pure ClearAllStatesParams
 
-instance Doc.DescribedParams ClearAllStatesParams where
+instance Doc.DescribedMethod ClearAllStatesParams () where
   parameterFieldDescription = []
 
 clearAllStatesDescr :: Doc.Block
diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs
index ba537997..c6cb6ca1 100644
--- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs
+++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ViewPatterns #-}
 module CryptolServer.Data.Expression
   ( module CryptolServer.Data.Expression
@@ -24,6 +25,7 @@ import qualified Data.Scientific as Sc
 import Data.Text (Text, pack)
 import qualified Data.Text as T
 import Data.Traversable
+import Data.Typeable (Proxy(..), typeRep)
 import qualified Data.Vector as V
 import Data.Text.Encoding (encodeUtf8)
 import Numeric (showHex)
@@ -49,6 +51,7 @@ import Cryptol.Utils.Ident
 import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)
 
 import Argo
+import qualified Argo.Doc as Doc
 import CryptolServer
 import CryptolServer.Exceptions
 import CryptolServer.Data.Type
@@ -235,6 +238,119 @@ instance JSON.ToJSON Expression where
     -- serialize Type PName that never gets called and just bitrots.
     toJSON gen
 
+instance Doc.Described Expression where
+  typeName = "JSON Cryptol Expressions"
+  description =
+    [ Doc.Paragraph [Doc.Text "In the API, Cryptol expressions can be represented by the following:"]
+    , Doc.DescriptionList
+        [ (pure $ Doc.Text "JSON Booleans",
+           Doc.Paragraph [Doc.Text "Represent the corresponding Cryptol Booleans"])
+        , (pure $ Doc.Text "JSON Integers",
+           Doc.Paragraph [Doc.Text "Cryptol integer literals, that can be used at a variety of types"])
+        , (pure $ Doc.Text "JSON Strings",
+           Doc.Paragraph [Doc.Text "Cryptol concrete syntax"])
+        , (pure $ Doc.Text "JSON Objects",
+           Doc.Paragraph [ Doc.Text "Objects can represent a variety of Cryptol expressions. The field "
+                         , Doc.Literal "expression"
+                         , Doc.Text " contains a tag that can be used to determine the remaining fields."
+                         ])
+        ]
+    , Doc.Paragraph [Doc.Text "The tag values in objects can be:"]
+    , Doc.DescriptionList
+        [ (pure $ Doc.Literal "bits",
+           Doc.BulletedList
+             [ Doc.Paragraph [Doc.Text "The expression is a bitvector. Further fields are:"]
+             , Doc.Paragraph [ Doc.Literal "encoding", Doc.Text ": Either the string "
+                             , Doc.Literal "base64", Doc.Text " or ", Doc.Literal "hex"
+                             , Doc.Text ", for base-64 or hexadecimal representations of the bitvector"
+                             ]
+             , Doc.Paragraph [Doc.Literal "data", Doc.Text ": A string containing the actual data"]
+             , Doc.Paragraph [Doc.Literal "width", Doc.Text ": An integer: the bit-width of the represented bit vector"]
+             ])
+        , (pure $ Doc.Literal "record",
+           Doc.Paragraph [ Doc.Text "The expression is a record. The field "
+                         , Doc.Literal "data", Doc.Text " is a JSON object that maps record field names to "
+                         , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expressions"
+                         , Doc.Text "."
+                         ])
+        , (pure $ Doc.Literal "sequence",
+           Doc.Paragraph [ Doc.Text "The expression is a sequence. The field "
+                         , Doc.Literal "data"
+                         , Doc.Text "contains a JSON array of the elements of the sequence; "
+                         , Doc.Text "each is a JSON Cryptol expression."
+                         ])
+        , (pure $ Doc.Literal "tuple",
+           Doc.Paragraph [ Doc.Text "The expression is a tuple. The field "
+                         , Doc.Literal "data"
+                         , Doc.Text "contains a JSON array of the elements of the tuple; "
+                         , Doc.Text "each is a JSON Cryptol expression."
+                         ])
+        , (pure $ Doc.Literal "unit",
+           Doc.Paragraph [Doc.Text "The expression is the unit constructor, and there are no further fields."])
+        , (pure $ Doc.Literal "let",
+           Doc.BulletedList
+             [ Doc.Paragraph [ Doc.Text "The expression is a ", Doc.Literal "where"
+                             , Doc.Text "binding. The fields are:"
+                             ]
+             , Doc.DescriptionList
+                 [ (pure $ Doc.Literal "binders",
+                    Doc.BulletedList
+                      [ Doc.Paragraph [Doc.Text "A list of binders. Each binder is an object with two fields:"]
+                      , Doc.Paragraph [ Doc.Literal "name"
+                                      , Doc.Text ": A string that is the name to be bound, and"
+                                      ]
+                      , Doc.Paragraph [ Doc.Literal "definition"
+                                      , Doc.Text "A "
+                                      , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
+                                      , Doc.Text "."
+                                      ]
+                     ])
+                 , (pure $ Doc.Literal "body",
+                    Doc.Paragraph [ Doc.Text "A "
+                                  , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
+                                  , Doc.Text " in which the bound names may be used."
+                                  ])
+                 ]
+             ])
+        , (pure $ Doc.Literal "call",
+           Doc.BulletedList
+             [ Doc.Paragraph [Doc.Text "The expression is a function application. Further fields are:"]
+             , Doc.Paragraph [ Doc.Literal "function", Doc.Text ": A "
+                             , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
+                             , Doc.Text "."
+                             ]
+             , Doc.Paragraph [ Doc.Literal "arguments", Doc.Text ": A JSON array of "
+                             , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expressions"
+                             , Doc.Text "."
+                             ]
+             ])
+        , (pure $ Doc.Literal "instantiate",
+           Doc.BulletedList
+             [ Doc.Paragraph [Doc.Text "The expression is a type application. Further fields are:"]
+             , Doc.Paragraph [ Doc.Literal "generic"
+                             , Doc.Text ": The polymorphic expression to be instantiated"
+                             ]
+             , Doc.Paragraph [ Doc.Literal "arguments"
+                             , Doc.Text ": A JSON object in which keys are the names of type parameters and values are "
+                             , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol types"
+                             , Doc.Text "."
+                             ]
+             ])
+        , (pure $ Doc.Literal "integer modulo",
+           Doc.BulletedList
+             [ Doc.Paragraph [ Doc.Text "The expression is an integer with a modulus (the Cryptol "
+                             , Doc.Literal "Z", Doc.Text " type). Further fields are:"
+                             ]
+             , Doc.Paragraph [ Doc.Literal "integer"
+                             , Doc.Text ": A JSON number, representing the integer"
+                             ]
+             , Doc.Paragraph [ Doc.Literal "modulus"
+                             , Doc.Text ": A JSON number, representing the modulus"
+                             ]
+             ])
+        ]
+    ]
+
 
 decode :: (Argo.Method m, Monad m) => Encoding -> Text -> m Integer
 decode Base64 txt =
diff --git a/cryptol-remote-api/src/CryptolServer/Data/Type.hs b/cryptol-remote-api/src/CryptolServer/Data/Type.hs
index b511f2ea..19e496f2 100644
--- a/cryptol-remote-api/src/CryptolServer/Data/Type.hs
+++ b/cryptol-remote-api/src/CryptolServer/Data/Type.hs
@@ -26,6 +26,8 @@ import Cryptol.Utils.Ident (mkIdent)
 import Cryptol.Utils.PP (pp)
 import Cryptol.Utils.RecordMap (canonicalFields)
 
+import qualified Argo.Doc as Doc
+
 
 newtype JSONSchema = JSONSchema Schema
 
@@ -294,3 +296,31 @@ instance JSON.FromJSON JSONPType where
       unaryPropF prop f o = unaryProp prop <$> typeField o f
       binTC tc f1 f2 o = tc <$> typeField o f1 <*> typeField o f2
       tyFun tf o = C.TUser (name tf) <$> typeListField o "arguments"
+
+instance Doc.Described JSONSchema where
+  typeName = "JSON Cryptol Types"
+  description =
+    [ Doc.Paragraph [Doc.Text "JSON representations of types are type schemas. A type schema has three fields:"]
+    , Doc.DescriptionList
+        [ (pure $ Doc.Literal "forall",
+           Doc.Paragraph [ Doc.Text "Contains an array of objects. Each object has two fields: "
+                         , Doc.Literal "name", Doc.Text " is the name of a type variable, and "
+                         , Doc.Literal "kind", Doc.Text " is its kind. There are four kind formers: the string "
+                         , Doc.Literal "Type", Doc.Text " represents ordinary datatypes, the string "
+                         , Doc.Literal "Num", Doc.Text " is the kind of numbers, and "
+                         , Doc.Literal "Prop", Doc.Text " is the kind of propositions. "
+                         , Doc.Text "Arrow kinds are represented by objects in which the field "
+                         , Doc.Literal "kind", Doc.Text " is the string "
+                         , Doc.Literal "arrow", Doc.Text ", and the fields "
+                         , Doc.Literal "from", Doc.Text " and ", Doc.Literal "to"
+                         , Doc.Text " are the kinds on the left and right side of the arrow, respectively."
+                         ])
+        , (pure $ Doc.Literal "propositions",
+           Doc.Paragraph [Doc.Text "A JSON array of the constraints in the type."])
+        , (pure $ Doc.Literal "type",
+           Doc.Paragraph [ Doc.Text "The type in which the variables from "
+                         , Doc.Literal "forall", Doc.Text " are in scope and the constraints in "
+                         , Doc.Literal "propositions", Doc.Text " are in effect."
+                         ])
+        ]
+    ]
diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs
index 77f6c585..fdd2c136 100644
--- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs
+++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs
@@ -1,4 +1,6 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
 module CryptolServer.EvalExpr
   ( evalExpression
   , evalExpressionDescr
@@ -9,6 +11,7 @@ module CryptolServer.EvalExpr
 import qualified Argo.Doc as Doc
 import Control.Monad.IO.Class
 import Data.Aeson as JSON
+import Data.Typeable (Proxy(..), typeRep)
 
 
 import Cryptol.ModuleSystem (checkExpr, evalExpr)
@@ -68,8 +71,23 @@ instance JSON.FromJSON EvalExprParams where
     JSON.withObject "params for \"evaluate expression\"" $
     \o -> EvalExprParams <$> o .: "expression"
 
-instance Doc.DescribedParams EvalExprParams where
+instance Doc.DescribedMethod EvalExprParams JSON.Value where
   parameterFieldDescription =
     [("expression",
       Doc.Paragraph [Doc.Text "The expression to evaluate."])
     ]
+
+  resultFieldDescription =
+    [ ("value",
+      Doc.Paragraph [ Doc.Text "A "
+                    , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
+                    , Doc.Text " that denotes the value"
+                    ])
+    , ("type",
+      Doc.Paragraph [ Doc.Text " A"
+                    , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type"
+                    , Doc.Text " that denotes the result type"
+                    ])
+    , ("type string",
+      Doc.Paragraph [Doc.Text "A human-readable representation of the result type"])
+    ]
diff --git a/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs b/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs
index eccd21dc..f4d37ff9 100644
--- a/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs
+++ b/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 module CryptolServer.ExtendSearchPath
   ( extSearchPath
@@ -31,7 +32,7 @@ instance FromJSON ExtendSearchPathParams where
     withObject "params for \"extend search path\"" $
     \o -> ExtendSearchPathParams <$> o .: "paths"
 
-instance Doc.DescribedParams ExtendSearchPathParams where
+instance Doc.DescribedMethod ExtendSearchPathParams () where
   parameterFieldDescription =
     [("paths",
       Doc.Paragraph [Doc.Text "The paths to add to the search path."])
diff --git a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs
index 318468c7..4ea5a6c3 100644
--- a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs
+++ b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 module CryptolServer.FocusedModule
   ( focusedModule
@@ -36,5 +37,18 @@ data FocusedModParams = FocusedModParams
 instance JSON.FromJSON FocusedModParams where
   parseJSON _ = pure FocusedModParams
 
-instance Doc.DescribedParams FocusedModParams where
+instance Doc.DescribedMethod FocusedModParams JSON.Value where
   parameterFieldDescription = []
+
+  resultFieldDescription =
+    [ ("module",
+      Doc.Paragraph [ Doc.Text "The name of the focused module, which would be shown in the "
+                    , Doc.Text "prompt in the Cryptol REPL, or "
+                    , Doc.Literal "null", Doc.Text " if there is no such focused module."
+                    ])
+    , ("parameterized",
+      Doc.Paragraph [ Doc.Text "A Boolean value indicating whether the focused module is "
+                    , Doc.Text "parameterized. This field is only present when the module name is not "
+                    , Doc.Literal "null", Doc.Text "."
+                    ])
+    ]
diff --git a/cryptol-remote-api/src/CryptolServer/LoadModule.hs b/cryptol-remote-api/src/CryptolServer/LoadModule.hs
index 7f924e59..1bd64849 100644
--- a/cryptol-remote-api/src/CryptolServer/LoadModule.hs
+++ b/cryptol-remote-api/src/CryptolServer/LoadModule.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 module CryptolServer.LoadModule
   ( loadFile
@@ -36,7 +37,7 @@ instance JSON.FromJSON LoadFileParams where
     \o -> LoadFileParams <$> o .: "file"
 
 
-instance Doc.DescribedParams LoadFileParams where
+instance Doc.DescribedMethod LoadFileParams () where
   parameterFieldDescription =
     [("file",
       Doc.Paragraph [Doc.Text "File path of the module to load."])
@@ -70,7 +71,7 @@ instance JSON.FromJSON LoadModuleParams where
     JSON.withObject "params for \"load module\"" $
     \o -> LoadModuleParams . unJSONModName <$> o .: "module name"
 
-instance Doc.DescribedParams LoadModuleParams where
+instance Doc.DescribedMethod LoadModuleParams () where
   parameterFieldDescription =
     [("module name",
       Doc.Paragraph [Doc.Text "Name of module to load."])
diff --git a/cryptol-remote-api/src/CryptolServer/Names.hs b/cryptol-remote-api/src/CryptolServer/Names.hs
index 1552d8c3..12b73e89 100644
--- a/cryptol-remote-api/src/CryptolServer/Names.hs
+++ b/cryptol-remote-api/src/CryptolServer/Names.hs
@@ -1,6 +1,9 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
 module CryptolServer.Names
   ( visibleNames
   , visibleNamesDescr
@@ -12,6 +15,7 @@ import Data.Aeson ((.=))
 import qualified Data.Map as Map
 import Data.Map (Map)
 import Data.Text (unpack)
+import Data.Typeable (Proxy(..), typeRep)
 
 import Cryptol.Parser.Name (PName(..))
 import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv)
@@ -31,9 +35,22 @@ data VisibleNamesParams = VisibleNamesParams
 instance JSON.FromJSON VisibleNamesParams where
   parseJSON _ = pure VisibleNamesParams
 
-instance Doc.DescribedParams VisibleNamesParams where
+instance Doc.DescribedMethod VisibleNamesParams [NameInfo] where
   parameterFieldDescription = []
 
+  resultFieldDescription =
+    [ ("name",
+      Doc.Paragraph [Doc.Text "A human-readable representation of the name"])
+    , ("type string",
+      Doc.Paragraph [Doc.Text "A human-readable representation of the name's type schema"])
+    , ("type",
+      Doc.Paragraph [ Doc.Text " A"
+                    , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type"
+                    ])
+    , ("documentation",
+      Doc.Paragraph [Doc.Text "An optional field containing documentation string for the name, if it is documented"])
+    ]
+
 visibleNamesDescr :: Doc.Block
 visibleNamesDescr =
   Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) names."]
diff --git a/cryptol-remote-api/src/CryptolServer/Options.hs b/cryptol-remote-api/src/CryptolServer/Options.hs
index e9ee3fb9..fe0310cc 100644
--- a/cryptol-remote-api/src/CryptolServer/Options.hs
+++ b/cryptol-remote-api/src/CryptolServer/Options.hs
@@ -1,8 +1,11 @@
 {-# OPTIONS_GHC -fno-warn-type-defaults -Wno-missing-deriving-strategies #-}
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
 module CryptolServer.Options (Options(..), WithOptions(..)) where
 
 import qualified Argo.Doc as Doc
@@ -73,8 +76,9 @@ instance FromJSON Options where
 data WithOptions a = WithOptions Options a
   deriving Functor
 
-instance forall params . Doc.DescribedParams params => Doc.DescribedParams (WithOptions params) where
-  parameterFieldDescription = (Doc.parameterFieldDescription @params)
+instance forall params result . Doc.DescribedMethod params result => Doc.DescribedMethod (WithOptions params) result where
+  parameterFieldDescription = Doc.parameterFieldDescription @params
+  resultFieldDescription    = Doc.resultFieldDescription @params @result
 
 instance FromJSON a => FromJSON (WithOptions a) where
   parseJSON = withObject "parameters with options" $
diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs
index a4224762..02d1f411 100644
--- a/cryptol-remote-api/src/CryptolServer/Sat.hs
+++ b/cryptol-remote-api/src/CryptolServer/Sat.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -168,7 +169,7 @@ instance FromJSON ProveSatParams where
                     Right int -> pure (SomeSat int)) v)
 
 
-instance Doc.DescribedParams ProveSatParams where
+instance Doc.DescribedMethod ProveSatParams ProveSatResult where
   parameterFieldDescription =
     [("prover",
       Doc.Paragraph ([Doc.Text "The SMT solver to use to check for satisfiability. I.e., one of the following: "]
@@ -195,3 +196,33 @@ instance Doc.DescribedParams ProveSatParams where
                     ]
       )
     ]
+
+  resultFieldDescription =
+    [ ("result",
+      Doc.Paragraph [ Doc.Text "A string (one of "
+                    , Doc.Literal "unsatisfiable", Doc.Text ", "
+                    , Doc.Literal "invalid", Doc.Text ", or "
+                    , Doc.Literal "satisfied"
+                    , Doc.Text ") indicating the result of checking for validity, satisfiability, or safety."
+                    ])
+    , ("counterexample type",
+      Doc.Paragraph $ onlyIfResultIs "invalid" ++
+                    [ Doc.Text "This describes the variety of counterexample that was produced. This can be either "
+                    , Doc.Literal "safety violation", Doc.Text " or ", Doc.Literal "predicate falsified", Doc.Text "."
+                    ])
+    , ("counterexample",
+      Doc.Paragraph $ onlyIfResultIs "invalid" ++
+                    [ Doc.Text "A list of objects where each object has an "
+                    , Doc.Literal "expr", Doc.Text "field, indicating a counterexample expression, and a "
+                    , Doc.Literal "type", Doc.Text "field, indicating the type of the expression."
+                    ])
+    , ("models",
+      Doc.Paragraph $ onlyIfResultIs "satisfied" ++
+                    [ Doc.Text "A list of list of objects where each object has an "
+                    , Doc.Literal "expr", Doc.Text "field, indicating a expression in a model, and a "
+                    , Doc.Literal "type", Doc.Text "field, indicating the type of the expression."
+                    ])
+    ]
+    where
+      onlyIfResultIs val = [ Doc.Text "Only used if the " , Doc.Literal "result"
+                           , Doc.Text " is ", Doc.Literal val, Doc.Text "." ]
diff --git a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs
index b9207b82..6477d836 100644
--- a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs
+++ b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs
@@ -1,4 +1,6 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
 module CryptolServer.TypeCheck
   ( checkType
   , checkTypeDescr
@@ -9,6 +11,7 @@ import qualified Argo.Doc as Doc
 
 --import Control.Lens hiding ((.=))
 import Data.Aeson as JSON
+import Data.Typeable
 
 import Cryptol.ModuleSystem (checkExpr)
 
@@ -39,8 +42,13 @@ instance JSON.FromJSON TypeCheckParams where
     JSON.withObject "params for \"check type\"" $
     \o -> TypeCheckParams <$> o .: "expression"
 
-instance Doc.DescribedParams TypeCheckParams where
+instance Doc.DescribedMethod TypeCheckParams JSON.Value where
   parameterFieldDescription =
     [("expression",
       Doc.Paragraph [Doc.Text "Expression to type check."])
     ]
+
+  resultFieldDescription =
+    [("type schema",
+      Doc.Paragraph [Doc.Text "A ", Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol Type"])
+    ]
diff --git a/deps/argo b/deps/argo
index 1040dc26..c7337181 160000
--- a/deps/argo
+++ b/deps/argo
@@ -1 +1 @@
-Subproject commit 1040dc26d142f13ff8ed6617ff5212f476b78c45
+Subproject commit c733718138c10c70c6e690d4a2de83a7b07e6cc9