definj-doc

(in-package "ACL2")

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