Def-fgl-program
Define a function that is logically just NIL but has special extralogical behavior in FGL.
Because of FGL's bind-var feature, it isn't always possible
to define a function the way you want it to run in FGL: if you want to use
bind-var, then you must have a free variable in the RHS of the equation
defining the function, which isn't allowed for ACL2 definitions. Instead, you
may provide a function definition without bind-var calls, disable that
definition for FGL (using disable-definition), and add an FGL rewrite
rule with def-fgl-rewrite that rewrites calls of the function to the body
containing the bind-var calls.
Def-fgl-program provides a convenient macro for this. It wraps define such that all the usual arguments for define may be used. It may also
contain the additional keyword args :equiv, giving the equivalence
relation for the generated rewrite rule (defaulting to unequiv), and
:fgl-hints, which allows hints to be passed to the proof for the rewrite
rule. Instead of providing the given function body as the body for the
define, it modifies it as follows: if :equiv is provided, it searches
the given body for calls of bind-var and syntax-bind and replaces
them with their second arguments; otherwise, it just provides a body of nil.
