defsurj-doc

(in-package "ACL2")

(defxdoc defsurj
  :parents (std/util defmapping)
  :short "Establish a surjective mapping between two domains."
  :long (topstring (p "This is a specialization of @(tsee defmapping) where
     the @(':alpha-of-beta-thm') input is @('t').
     See the documentation of @(tsee defmapping).")
    (p "Here `surjective' refers to the @($\alpha$) conversion.
     Its right inverse conversion @($\beta$) is injective.")))