... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/.

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

(the .public documentation
  (List $.Documentation)
  (list ($.module /._
                  "Type-checking functionality.")

        ($.definition /.unknown_type_var)
        ($.definition /.unbound_type_var)
        ($.definition /.invalid_type_application)
        ($.definition /.cannot_rebind_var)
        ($.definition /.type_check_failed)
        ($.definition /.functor)
        ($.definition /.apply)
        ($.definition /.monad)
        ($.definition /.bound?)
        ($.definition /.peek)
        ($.definition /.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 /.value
          ""
          ($.example (' (value context proc))))

        ($.definition /.failure
          ""
          ($.example (' (failure message))))

        ($.definition /.assertion
          ""
          ($.example (' (assertion message test))))

        ($.definition /.except
          ""
          ($.example (' (except exception message))))

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

        ($.definition /.bind
          (%.message "Attemmpts to buy a type-variable."
                     \n "Fails if the variable has been bound already.")
          ($.example (' (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."
          ($.example (' (check expected actual))))

        ($.definition /.subsumed?
          "A simple type-checking function that just returns a yes/no answer."
          ($.example (' (subsumed? 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."
          ($.example (' (clean inputT))))
        ))
