我在 ACL2 中定义一个（is-related）函数时有点挣扎。有人告诉我它可以在一行中完成，但我不确定如何做到这一点。目标是定义函数（is-related xy R）。请记住，关系是对的列表，因此例如 R 可能如下所示：
((a 1) (a 2) (b 1) (b 3) )
在这种情况下，
(is-related 'a 1 R) = T
(is-related 'a 3 R) = NIL
提示：这应该很容易编码，只需一行代码即可。
我曾尝试将该函数definec contains 与 a 一起使用，if-then-else statment但它肯定比一行代码长。我对如何做到这一点进行了一些研究，并且不断收到使用建议，defthm 但我认为这不是问题所要求的。任何帮助，将不胜感激！