		Search-engine friendly clone of the ACL2 documentation.

Ctrex-rule

This is a product type introduced by defprod.

name — symbolp
assigned-var — pseudo-var: Variable name standing for the object whose value is determined by an application of this rule
assign — pseudo-term: Value to be assigned to assigned-var, in terms of the assigned-var itself and variables both used and bound in match, and keys of match-conds. Possible restriction: elim rules should only use the keys of match/match-conds, not e.g. the assigned-var
match — cmr::pseudo-term-subst: Substitution giving values to variables. When we make the cgraph, addition of an edge with this rule is triggered when a cgraph node matches one of the terms in the substitution.
match-conds — cmr::pseudo-term-subst: Each key will be assigned T if its value/match variable has an assignment after recurring over the match expressions.
assign-cond — pseudo-term: Condition under which to perform the assignment, in terms of the same variables as assign
hyp — pseudo-term
equiv — pseudo-fnsym
ruletype — ctrex-ruletype-p