Expand description
Encoding of Rustbelt’s lifetime logic in Creusot.
The main types are FullBorrow and LifetimeToken; the first is
a mutable borrow whose lifetime is tracked by Creusot rather than by the
compiler. This lifetime is represented by a LifetimeToken object.
Structs§
- EndBorrow
- Container for the final value of a
FullBorrow. - Full
Borrow - A mutable borrow, with a synthetic lifetime.
- Lifetime
- Abstract representation of a lifetime.
- Lifetime
Dead - A lifetime that has expired.
- Lifetime
Token - A token signaling that the corresponding lifetime is still active.