dafny_runtime

Type Alias DafnyString

Source
pub type DafnyString = Sequence<DafnyChar>;

Aliased Type§

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

Variants§

§

ArraySequence

Fields

§values: Rc<Vec<DafnyChar>>
§

ConcatSequence