Vl-timetoken-p
Tokens for time literals, like 3ns or 45.617us.
(vl-timetoken-p x) is a defaggregate of the following fields.
- etext — The characters that gave rise to this token.
Invariant (and (vl-echarlist-p etext) (consp etext)).
- quantity — An ACL2 string with the amount. In practice, the amount should
match either unsigned_number or fixed_point_number,
e.g., "3" or "45.617". We don't try to process
this further because (1) we don't expect it to matter for much,
and (2) ACL2 doesn't really support fixed point numbers.
Invariant (stringp quantity).
- units — The kind of time unit this is, e.g., seconds, milliseconds,
microseconds, ...
Invariant (vl-timeunit-p units).
- breakp — Was this the first token on a line.
Invariant (booleanp breakp).
Source link: vl-timetoken-p
Subtopics
- Vl-timetoken
- Raw constructor for vl-timetoken-p structures.
- Make-vl-timetoken
- Constructor macro for vl-timetoken-p structures.
- Change-vl-timetoken
- A copying macro that lets you create new vl-timetoken-p structures, based on existing structures.
- Make-honsed-vl-timetoken
- Constructor macro for honsed vl-timetoken-p structures.
- Honsed-vl-timetoken
- Raw constructor for honsed vl-timetoken-p structures.
- Vl-timetoken->units
- Access the units field of a vl-timetoken-p structure.
- Vl-timetoken->quantity
- Access the quantity field of a vl-timetoken-p structure.
- Vl-timetoken->etext
- Access the etext field of a vl-timetoken-p structure.
- Vl-timetoken->breakp
- Access the breakp field of a vl-timetoken-p structure.
