math_sequence.bend checks

raw source on the hub · import stelliferous@0.0.2.0/math_sequence.bend as Math_sequence

Element- and length-indexed sequence model. Random get is O(index); runtime dense storage is Array<Element>, not this sequential observation.

1 import

import Base

Laws

law Values provedsource · line 5 · raw

@-Element:Data -> @length:Nat -> Data

law Index provedsource · line 18 · raw

@length:Nat -> Data

Types

type Elements source · line 10 · raw

@-Element:Data -> @-length:Nat -> Data

Elements

@-Element:Data -> @-length:Nat -> @head:Element -> @tail:Values(Element, length) -> Elements<Element, length>

type Position source · line 22 · raw

@-length:Nat -> Data

First
```
@-length:Nat -> Position<length>
```

Next

@-length:Nat -> @index:Index(length) -> Position<length>

Definitions

def index_value source · line 31 · raw

@length:Nat -> @index:Index(length) -> Nat

def get source · line 46 · raw

@-Element:Data -> @length:Nat -> @index:Index(length) -> @vector:Values(Element, length) -> Element

def replicate source · line 59 · raw

@-Element:Data -> @length:Nat -> @+value:Element -> Values(Element, length)

Templates

template tabulate source · line 40 · raw

@-Element:Data -> @-Context:Data -> @-sample:(@_:Context -> @_:Nat -> Element) -> @length:Nat -> @+offset:Nat -> @+context:Context -> Values(Element, length)

template zip_map source · line 65 · raw

@-Element:Data -> @-Context:Data -> @-combine:(@_:Context -> @_:Element -> @_:Element -> Element) -> @length:Nat -> @+context:Context -> @left:Values(Element, length) -> @right:Values(Element, length) -> Values(Element, length)