[][src]Module spec_lang::ast

Contains AST definitions for the specification language fragments of the Move language.

Structs

Condition
ExpDisplay

Helper type for expression display.

GlobalInvariant

Describes a global invariant.

LocalVarDecl
ModuleName

Names

ModuleNameDisplay

A helper to support module names in formatting.

QualifiedSymbol
QualifiedSymbolDisplay

A helper to support qualified symbols in formatting.

Spec

Specification and properties associated with a language item.

SpecBlockInfo

Information about a specification block in the source. This is used for documentation generation. In the object model, the original locations and documentation of spec blocks is reduced to conditions on a Spec, with expansion of schemas. This data structure allows us to discover the original spec blocks and their content.

SpecFunDecl
SpecVarDecl

Declarations

Enums

ConditionKind

Conditions

Exp

Expressions

Operation
SpecBlockTarget

Describes the target of a spec block.

Value

Type Definitions

PropertyBag

Specifications