ibody

(in-package "ACL2")

(define ibody
  ((fn symbolp) (wrld plist-worldp))
  :returns (body "An untranslated term.")
  :mode :program :parents (std/system/function-queries)
  :short "Retrieve the untranslated body of a function."
  :long (topstring (p "This is as introduced (hence the @('i') in the name) by the user."))
  (car (last (get-defun-event fn wrld))))