Skip to main content

charon_lib/ast/type_level/
regions.rs

1use crate::ast::*;
2use derive_generic_visitor::*;
3use macros::{EnumAsGetters, EnumIsA};
4use serde_state::{DeserializeState, SerializeState};
5
6#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
7#[derive(EnumIsA, EnumAsGetters)]
8#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
9#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("R"))]
10pub enum Region {
11    /// Region variable. See `DeBruijnVar` for details.
12    Var(RegionDbVar),
13    /// Static region
14    Static,
15    /// Body-local region, considered existentially-bound at the level of a body.
16    Body(RegionId),
17    /// Erased region
18    Erased,
19}