Enum AttrKind 

pub enum AttrKind {
    Chain,
    Priority,
    Tag(Ident),
}

A kind of attribute that can be applied to a term declaration or rule.

Variants

Chain

In verification, apply rule chaining to this term.

A term marked for chaining may omit a specification. Instead, all possible applications of rules to this term will be generated and verified.

Priority

In verification, declare that the correctness of lower priority rules depends on this rule not matching.

During rule expansion, any higher-priority overlapping rules that have the priority tag will have their match conditions negated and added to the verification conditions.

Note that care must be taken when using this tag: if the specification for the match conditions of the higher priority rule are an over-approximation of reality, then the assumptions made by lower priority rules will be an under-approximation. In an extreme case this may cause the verifier to determine the lower priority rule never applies. In a more subtle case, it could cause bugs to be missed.

Tag(Ident)

Tag allows for categorizing terms and rules.

Trait Implementations

impl Clone for AttrKind

fn clone(&self) -> AttrKind

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AttrKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for AttrKind

impl PartialEq for AttrKind

fn eq(&self, other: &AttrKind) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for AttrKind

impl ToSExpr for AttrKind

fn to_sexpr(&self) -> SExpr

Convert the given value to an S-expression.