Enum SyntaxAttr 

enum SyntaxAttr {
    Reft,
    Invariant(Expr),
    RefinedBy(RefineParams),
    Hide,
}

An attribute that’s considered part of the syntax of an item.

This is in contrast to a surface::Attr which changes the behavior of an item. For example, a #[refined_by(...)] is part of the syntax of an adt: we could think of a different syntax that doesn’t use an attribute. The existence of a syntax attribute in the token stream can be used to decide how to keep parsing, for example, if we see a #[reft] we know that the next item bust be an associated refinement and not a method inside an impl or trait.

Variants

Reft

A #[reft] attribute

Invariant(Expr)

A #[invariant] attribute

RefinedBy(RefineParams)

A #[refined_by(...)] attribute

Hide

A #[hide] attribute

NOTE(nilehmann) This should be considered a normal attribute, but we haven’t implemented attributes for flux items. If we start seeing more of these we should consider implementing the infrastructure necesary to keep a list of attributes inside the flux item like we do for rust items.