		Search-engine friendly clone of the ACL2 documentation.

Fgl-rewrite-rules

Fgl-hide

FGL function that inhibits rewriting of its subterm

Signature
(fgl-hide term) → *

This acts more or less like hide in ACL2. Its subterm is processed by the FGL interpreter, except that whenever a non-FGL-special function call is processed, it is just turned into a g-apply form. The fgl-hide call itself is not turned into a g-apply, but just replaced by the object resulting from this processing of its subterm.

Definitions and Theorems

Function: fgl-hide

(defun fgl-hide (term)
  (declare (xargs :guard t))
  (let ((__function__ 'fgl-hide))
    (declare (ignorable __function__))
    term))