		Search-engine friendly clone of the ACL2 documentation.

Vl-propeventually

An eventually or s_eventually property expression.

This is a product type, introduced by deftagsum in support of vl-propexpr.

strongp — booleanp: True when this is an s_eventually.
range — vl-maybe-range: The range applied to this eventually, if applicable. For instance, in eventually [2:3] foo, the range is [2:3]. In the grammar, ranges are optional for s_eventually but are required for ordinary eventually properties. We don't enforce this in our data structures, but it is enforced by the parser.
prop — vl-propexpr: The property being tested, e.g., foo in eventually foo.

Vl-propeventually->strongp: Get the strongp field from a vl-propeventually.
Vl-propeventually->range: Get the range field from a vl-propeventually.
Vl-propeventually->prop: Get the prop field from a vl-propeventually.
Make-vl-propeventually: Basic constructor macro for vl-propeventually structures.
Change-vl-propeventually: Modifying constructor for vl-propeventually structures.