Module move_ir_types::spec_language_ast

Structs

• Invariant_
  An invariant over a resource.
• SyntheticDefinition_
  A synthetic variable definition.

Enums

• Condition_
  A specification directive to be verified
• FieldOrIndex
  AST for the Move Prover specification language.
• SpecExp
  An expression in the specification language
• StorageLocation
  A location that can store a value

Type Definitions

• Condition
  Specification directive with span.
• Invariant
  Invariant with span.
• SyntheticDefinition
  Synthetic with span.