## Summary Port [`base_logic/lib/token.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/base_logic/lib/token.v). ## Dependencies **Rocq dependencies:** - `proofmode/proofmode` (aggregation) - #228 - #265
Summary
Port
base_logic/lib/token.v.Dependencies
Rocq dependencies:
proofmode/proofmode(aggregation)