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