布尔运算符，一等函数

Question

似乎内置布尔运算符不是 Dafny 中的一流函数，因为以下代码无法编译。我错过了什么吗？作为一种变通方法，我假设我们可以将内置函数包装在我们自己的函数中。

datatype binOp = X 

function evalOp(o: binOp): bool -> bool
{
    match o
    {
        case X => &&
    }
}

顺便说一句，错误消息是“Invalid UnaryExpression”。

Answer 1

不，Dafny 不会将 && 之类的运算符视为函数值。

如您所料，您可以包装运算符来创建一个函数。在您的示例中，这样的事情可能会起作用。

case X => (x, y) => x && y

如果您打算经常使用该函数，您可能更愿意为其命名。