model.bend checks
raw source on the hub · import 0xd684886d10b431b9dce6c3b2d1ef1980/model.bend as Model
1 import
import Base
Types
type Op source · line 4 · raw
Data
Independent sequence model. No implementation imports or array operations.
Push@x:U32 -> Op
PopOp
Get@i:U32 -> Op
Set@i:U32 -> @x:U32 -> Op
Swap@i:U32 -> @x:U32 -> Op
Reserve@minimum:U32 -> Op
Slice@start:U32 -> @end:U32 -> Op
type Observation source · line 13 · raw
Data
OkObservation
Value@x:U32 -> Observation
Values@xs:List<&2, U32> -> Observation
BadIndexObservation
IsEmptyObservation
AtLimitObservation
BadRangeObservation
type State source · line 22 · raw
Data
Sequence@items:List<&2, U32> -> @max:U32 -> State
Definitions
def length source · line 25 · raw
@xs:List<&2, U32> -> U32
def append source · line 28 · raw
@xs:List<&2, U32> -> @value:U32 -> List<&2, U32>
def get source · line 35 · raw
@xs:List<&2, U32> -> @i:Nat -> Observation
def set source · line 46 · raw
@xs:List<&2, U32> -> @i:Nat -> @value:U32 -> List<&2, U32>
def pop_tail source · line 57 · raw
@x:U32 -> @pair:Pair(List<&2, U32>, Observation) -> Pair(List<&2, U32>, Observation)
def pop source · line 61 · raw
@xs:List<&2, U32> -> Pair(List<&2, U32>, Observation)
def popped source · line 72 · raw
@max:U32 -> @pair:Pair(List<&2, U32>, Observation) -> Pair(State, Observation)
def push_if source · line 76 · raw
@+xs:List<&2, U32> -> @+max:U32 -> @x:U32 -> @valid:Bool -> Pair(State, Observation)
def set_if source · line 83 · raw
@+xs:List<&2, U32> -> @max:U32 -> @i:U32 -> @x:U32 -> @valid:Bool -> Pair(State, Observation)
def swap_if source · line 90 · raw
@+xs:List<&2, U32> -> @max:U32 -> @+i:U32 -> @x:U32 -> @valid:Bool -> Pair(State, Observation)
def reserve_if source · line 97 · raw
@xs:List<&2, U32> -> @max:U32 -> @valid:Bool -> Pair(State, Observation)
def slice_if source · line 104 · raw
@+xs:List<&2, U32> -> @max:U32 -> @+start:U32 -> @end:U32 -> @valid:Bool -> Pair(State, Observation)
def step source · line 111 · raw
@state:State -> @op:Op -> Pair(State, Observation)
def list_eq source · line 130 · raw
@xs:List<&2, U32> -> @ys:List<&2, U32> -> Bool
def obs_eq source · line 145 · raw
@x:Observation -> @y:Observation -> Bool