(.require
 [library
  [lux (.except and)
   ["$" documentation]
   [data
    ["[0]" text (.only \n)
     ["%" \\format (.only format)]]]]]
 [\\library
  ["[0]" /]])

(.def .public documentation
  (.List $.Module)
  ($.module /._
            "Type-checking functionality."
            [($.default /.unknown_type_var)
             ($.default /.unbound_type_var)
             ($.default /.invalid_type_application)
             ($.default /.cannot_rebind_var)
             ($.default /.type_check_failed)
             ($.default /.functor)
             ($.default /.apply)
             ($.default /.monad)
             ($.default /.bound?)
             ($.default /.peek)
             ($.default /.read)

             ($.definition /.Var
               "The ID for a type-variable in a type-checking context.")

             ($.definition (/.Check it)
               "A type-checking computation which may fail or yield a value.")

             ($.definition /.result
               ""
               [(result context proc)])

             ($.definition /.failure
               ""
               [(failure message)])

             ($.definition /.assertion
               ""
               [(assertion message test)])

             ($.definition /.except
               ""
               [(except exception message)])

             ($.definition /.existential
               "A brand-new existential type.")

             ($.definition /.bind
               (format "Attemmpts to buy a type-variable."
                       \n "Fails if the variable has been bound already.")
               [(bind type id)])

             ($.definition /.var
               "A brand-new (unbound) type-variable.")

             ($.definition /.fresh_context
               "An empty/un-used type-checking context.")

             ($.definition /.check
               "Type-check to ensure that the 'expected' type subsumes the 'actual' type."
               [(check expected actual)])

             ($.definition /.subsumes?
               "A simple type-checking function that just returns a yes/no answer."
               [(subsumes? expected actual)])

             ($.definition /.context
               "The current state of the type-checking context.")

             ($.definition /.clean
               "Resolves every bound type-variable to yield a new type that is as resolved as possible."
               [(clean inputT)])]
            []))