DafnyString

Type Alias DafnyString 

Source
pub type DafnyString = Sequence<DafnyChar>;

Aliased Type§

pub enum DafnyString {
    ArraySequence {
        values: Rc<Vec<DafnyChar>>,
    },
    ConcatSequence {
        left: Rc<RefCell<Sequence<DafnyChar>>>,
        right: Rc<RefCell<Sequence<DafnyChar>>>,
        length: usize,
        cache: Rc<RefCell<Option<Rc<Vec<DafnyChar>>>>>,
    },
}

Variants§

§

ArraySequence

Fields

§values: Rc<Vec<DafnyChar>>
§

ConcatSequence