seq -- Documentation

Seq

Seq;defined in: seq.key Line: 12 Offset :4

seqPerm

seqPerm (Seq , Seq ); defined in: seq.key Line: 16 Offset :4

seqNPerm

seqNPerm (Seq ); defined in: seq.key Line: 17 Offset :4

alpha::seqGet

alpha alpha :: seqGet (Seq , int ); defined in: seq.key Line: 22 Offset :4

seqLen

int seqLen (Seq ); defined in: seq.key Line: 23 Offset :4

seqIndexOf

int seqIndexOf (Seq , any ); defined in: seq.key Line: 24 Offset :4

seqGetOutside

any seqGetOutside ; defined in: seq.key Line: 25 Offset :4

seqEmpty

Seq seqEmpty ; defined in: seq.key Line: 28 Offset :4

seqSingleton

Seq seqSingleton (any ); defined in: seq.key Line: 29 Offset :4

seqConcat

Seq seqConcat (Seq , Seq ); defined in: seq.key Line: 30 Offset :4

seqSub

Seq seqSub (Seq , int , int ); defined in: seq.key Line: 31 Offset :4

seqReverse

Seq seqReverse (Seq ); defined in: seq.key Line: 32 Offset :4

seqUpd

Seq seqUpd (Seq , int , any ); defined in: seq.key Line: 33 Offset :4

seqDef

Seq seqDef {false , false , true } (int , int , any ); defined in: seq.key Line: 34 Offset :4

seqSwap

Seq seqSwap (Seq , int , int ); defined in: seq.key Line: 36 Offset :4

seqRemove

Seq seqRemove (Seq , int ); defined in: seq.key Line: 37 Offset :4

seqNPermInv

Seq seqNPermInv (Seq ); defined in: seq.key Line: 38 Offset :4

array2seq

Seq array2seq (Heap , Object ); defined in: seq.key Line: 40 Offset :4

values

Seq values ; defined in: seq.key Line: 43 Offset :4

seq_def_workaround

Seq seq_def_workaround (Heap , int , int , Object ); defined in: seq.key Line: 46 Offset :4

seq_def_workaround2

Seq seq_def_workaround2 (Heap , int , int , Object , LocSet ); defined in: seq.key Line: 47 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview

seq.key

Sorts

Seq

Predicates