Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
!988
Naming convention about lookup/elem_of.
Code
Review changes
Check out branch
Download
Patches
Plain diff
Robbert Krebbers
requested to merge
robbert/naming_order
into
master
Sep 21, 2023
Overview
2
Commits
2
Pipelines
2
Changes
1
Expand
See discussion in
stdpp!506 (comment 96086)
Edited
Sep 21, 2023
by
Robbert Krebbers
Merge request reports