logic

    Dark Mode
Search:
Group by:

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