From f5d2b9b89a4a45ba33bd187efcb462b6070f8d88 Mon Sep 17 00:00:00 2001 From: J Sailor Date: Sun, 28 Aug 2022 20:49:52 -0400 Subject: [PATCH] fix typo in comment defining macros (#6306) The existing comment describes macros as "formulas of the form `(forall X (= (f X) T[X]))` ... where `T[X]` does not contain `X`". This is incorrect; of course the macros' definitions are allowed to be in terms of the macros' arguments. The comment should say "...does not contain `f`" because macros can't be recursive. --- src/ast/macros/macro_manager.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h index 8f7d0c4b1..57583b67b 100644 --- a/src/ast/macros/macro_manager.h +++ b/src/ast/macros/macro_manager.h @@ -29,7 +29,7 @@ Revision History: \brief Macros are universally quantified formulas of the form: (forall X (= (f X) T[X])) (forall X (iff (f X) T[X])) - where T[X] does not contain X. + where T[X] does not contain f. This class is responsible for storing macros and expanding them. It has support for backtracking and tagging declarations in an expression as forbidded for being macros.