Vl-time
Representation of time amounts.
This is a product type introduced by defprod.
Fields
- quantity — stringp
- 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.
- units — vl-timeunit-p
- The kind of time unit this is, e.g., seconds, milliseconds,
microseconds, ...
We barely support this. You should probably not rely on our
current representation, since we will almost certainly want to change it as
soon as we do anything with time units.
Subtopics
- Vl-time-fix
- Fixing function for vl-time structures.
- Vl-time-equiv
- Basic equivalence relation for vl-time structures.
- Make-vl-time
- Basic constructor macro for vl-time structures.
- Vl-time->quantity
- Get the quantity field from a vl-time.
- Vl-time->units
- Get the units field from a vl-time.
- Change-vl-time
- Modifying constructor for vl-time structures.
- Vl-time-p
- Recognizer for vl-time structures.
