This module provides further logic operators like 'forall' and 'exists' They are only supported in .ensures etc pragmas.
proc `->`(a, b: bool): bool {.magic: "Implies", ...raises: [], tags: [], forbids: [].}
proc `<->`(a, b: bool): bool {.magic: "Iff", ...raises: [], tags: [], forbids: [].}
proc exists(args: varargs[untyped]): bool {.magic: "Exists", ...raises: [], tags: [], forbids: [].}
proc forall(args: varargs[untyped]): bool {.magic: "Forall", ...raises: [], tags: [], forbids: [].}
proc old[T](x: T): T {.magic: "Old", ...raises: [], tags: [], forbids: [].}