Language shapes catalog

September 12, 2026 · View on GitHub

Status: generated from examples/*.spx through the semaprax doc documentation model by tests/projections.rs::shapes_catalog; edit the examples, then regenerate with cargo test --locked -p semaprax --test projections -- --ignored shapes_catalog::regenerate_shapes_catalog.

Audience: agents and humans writing SEMAPRAX declarations from an installed compiler.

Every shape below is the canonical header of a declaration in a committed, verified example, rendered by the same documentation model as semaprax doc, so the catalog cannot show a shape the compiler rejects. semaprax help shapes prints this document. The agent quick reference explains the rules behind the shapes, and Documentation Projection v1 owns the model. Identities are the examples' own @id attributes; bodies are omitted.

Records

`ledger.account` (`examples/banking_ledger.spx`)

@id("ledger.account")
record Account {
    @id("ledger.account.id")
    id: i64,
    @id("ledger.account.balance")
    balance: i64,
}

`byte.type` (`examples/bytes_u8.spx`)

@id("byte.type")
record Sample {
    @id("byte.tag")
    tag: u8,
    @id("byte.weight")
    weight: i64,
}

`glyph.type` (`examples/chars.spx`)

@id("glyph.type")
record Glyph {
    @id("glyph.symbol")
    symbol: char,
    @id("glyph.weight")
    weight: i64,
}

`expr.pair` (`examples/expression_evaluator.spx`)

@id("expr.pair")
record Pair {
    @id("expr.pair.left")
    left: i64,
    @id("expr.pair.right")
    right: i64,
}

`geometry.point` (`examples/field_mutation.spx`)

@id("geometry.point")
record Point {
    @id("geometry.point.x")
    x: i64,
    @id("geometry.point.y")
    y: i64,
    @id("geometry.point.enabled")
    enabled: bool,
}

`geometry.vector` (`examples/floats.spx`)

@id("geometry.vector")
record Vector {
    @id("geometry.vector.x")
    x: f64,
    @id("geometry.vector.y")
    y: f64,
}

`order.line` (`examples/order_lifecycle.spx`)

@id("order.line")
record Line {
    @id("order.line.sku")
    sku: i64,
    @id("order.line.quantity")
    quantity: i64,
    @id("order.line.unit_price")
    unit_price: i64,
}

`geometry.point` (`examples/records.spx`)

@id("geometry.point")
record Point {
    @id("geometry.point.x")
    x: i64,
    @id("geometry.point.y")
    y: i64,
    @id("geometry.point.enabled")
    enabled: bool,
}

`geometry.line` (`examples/records.spx`)

@id("geometry.line")
record Line {
    @id("geometry.line.start")
    start: Point,
    @id("geometry.line.end")
    end: Point,
}

Variants

`ledger.tx_kind` (`examples/banking_ledger.spx`)

@id("ledger.tx_kind")
variant TxKind {
    @id("ledger.tx_kind.deposit")
    Deposit,
    @id("ledger.tx_kind.withdraw")
    Withdraw,
    @id("ledger.tx_kind.transfer")
    Transfer,
}

`expr.op` (`examples/expression_evaluator.spx`)

@id("expr.op")
variant Op {
    @id("expr.op.add")
    Add,
    @id("expr.op.subtract")
    Subtract,
    @id("expr.op.multiply")
    Multiply,
    @id("expr.op.divide")
    Divide,
}

`expr.unary` (`examples/expression_evaluator.spx`)

@id("expr.unary")
variant UnaryOp {
    @id("expr.unary.negate")
    Negate,
    @id("expr.unary.double")
    Double,
}

`order.status` (`examples/order_lifecycle.spx`)

@id("order.status")
variant Status {
    @id("order.status.created")
    Created,
    @id("order.status.paid")
    Paid,
    @id("order.status.shipped")
    Shipped,
    @id("order.status.delivered")
    Delivered,
    @id("order.status.cancelled")
    Cancelled,
}

`order.decision` (`examples/order_lifecycle.spx`)

@id("order.decision")
variant Decision {
    @id("order.decision.approve")
    Approve,
    @id("order.decision.reject")
    Reject,
    @id("order.decision.hold")
    Hold,
}

Classes

`ledger.portfolio` (`examples/banking_ledger.spx`)

@id("ledger.portfolio")
class Portfolio {
    @id("ledger.portfolio.holdings")
    holdings: i64,
    @id("ledger.portfolio.credits")
    credits: i64,

    @id("ledger.portfolio.total")
    fn total(self: Portfolio) -> i64

    @id("ledger.portfolio.deposited")
    fn deposited(self: Portfolio, amount: i64) -> Portfolio

    @id("ledger.portfolio.charged")
    fn charged(self: Portfolio, amount: i64) -> Portfolio
}

`example.counter` (`examples/classes.spx`)

@id("example.counter")
class Counter {
    @id("example.counter.value")
    value: i64,

    @id("example.counter.get")
    fn get(self: Counter) -> i64

    @id("example.counter.bumped")
    fn bumped(self: Counter, amount: i64) -> Counter
}

`example.counter` (`examples/field_mutation.spx`)

@id("example.counter")
class Counter {
    @id("example.counter.value")
    value: i64,

    @id("example.counter.get")
    fn get(self: Counter) -> i64
}

`example.animal` (`examples/inheritance.spx`)

@id("example.animal")
class Animal {
    @id("example.animal.legs")
    legs: i64,

    @id("example.animal.speak")
    fn speak(self: Animal) -> i64

    @id("example.animal.name")
    fn name(self: Animal) -> string
}

`example.dog` (`examples/inheritance.spx`)

@id("example.dog")
class Dog : Animal {
    @id("example.dog.bark_count")
    bark_count: i64,

    @id("example.dog.speak")
    fn speak(self: Dog) -> i64

    @id("example.dog.name")
    fn name(self: Dog) -> string
}

`example.puppy` (`examples/inheritance.spx`)

@id("example.puppy")
class Puppy : Dog {
    @id("example.puppy.cuteness")
    cuteness: i64,

    @id("example.puppy.total")
    fn total(self: Puppy) -> i64
}

`order.inventory` (`examples/order_lifecycle.spx`)

@id("order.inventory")
class Inventory {
    @id("order.inventory.stock")
    stock: i64,
    @id("order.inventory.reserved")
    reserved: i64,

    @id("order.inventory.available")
    fn available(self: Inventory) -> i64

    @id("order.inventory.reserve")
    fn reserve(self: Inventory, amount: i64) -> Inventory

    @id("order.inventory.commit")
    fn commit(self: Inventory, amount: i64) -> Inventory
}

Methods

`ledger.portfolio.total` (`examples/banking_ledger.spx`)

@id("ledger.portfolio.total")
fn total(self: Portfolio) -> i64

`ledger.portfolio.deposited` (`examples/banking_ledger.spx`)

@id("ledger.portfolio.deposited")
fn deposited(self: Portfolio, amount: i64) -> Portfolio

`ledger.portfolio.charged` (`examples/banking_ledger.spx`)

@id("ledger.portfolio.charged")
fn charged(self: Portfolio, amount: i64) -> Portfolio

`example.counter.get` (`examples/classes.spx`)

@id("example.counter.get")
fn get(self: Counter) -> i64

`example.counter.bumped` (`examples/classes.spx`)

@id("example.counter.bumped")
fn bumped(self: Counter, amount: i64) -> Counter

`example.counter.get` (`examples/field_mutation.spx`)

@id("example.counter.get")
fn get(self: Counter) -> i64

`example.animal.speak` (`examples/inheritance.spx`)

@id("example.animal.speak")
fn speak(self: Animal) -> i64

`example.animal.name` (`examples/inheritance.spx`)

@id("example.animal.name")
fn name(self: Animal) -> string

`example.dog.speak` (`examples/inheritance.spx`)

@id("example.dog.speak")
fn speak(self: Dog) -> i64

`example.dog.name` (`examples/inheritance.spx`)

@id("example.dog.name")
fn name(self: Dog) -> string

`example.puppy.total` (`examples/inheritance.spx`)

@id("example.puppy.total")
fn total(self: Puppy) -> i64

`order.inventory.available` (`examples/order_lifecycle.spx`)

@id("order.inventory.available")
fn available(self: Inventory) -> i64

`order.inventory.reserve` (`examples/order_lifecycle.spx`)

@id("order.inventory.reserve")
fn reserve(self: Inventory, amount: i64) -> Inventory

`order.inventory.commit` (`examples/order_lifecycle.spx`)

@id("order.inventory.commit")
fn commit(self: Inventory, amount: i64) -> Inventory

Resources

`platform.token` (`examples/lifecycle.spx`)

@id("platform.token")
resource Token {
    @id("platform.token.drop")
    drop import "platform.token.finalize";
}

`example.token` (`examples/native_callable.spx`)

@id("example.token")
resource Token {
    @id("example.token.drop")
    drop trivial;
}

`buffer.type` (`examples/ownership.spx`)

@id("buffer.type")
resource Buffer {
    @id("buffer.type.drop")
    drop trivial;
}

Interfaces

`platform.token.host` (`examples/lifecycle.spx`)

@id("platform.token.host")
interface TokenHost
    permits { platform.token.release }
{
    @id("platform.token.finalize")
    import fn finalize(token: own Token) -> unit
        effects { platform.token.release }
        failure infallible
        consumes token always;
}

Functions

`ledger.is_deposit` (`examples/banking_ledger.spx`)

@id("ledger.is_deposit")
fn is_deposit(kind: TxKind) -> bool

`ledger.apply` (`examples/banking_ledger.spx`)

@id("ledger.apply")
fn apply(account: Account, kind: TxKind, amount: i64) -> Account
    requires amount >= 0

`ledger.safe_withdraw` (`examples/banking_ledger.spx`)

@id("ledger.safe_withdraw")
fn safe_withdraw(account: Account, amount: i64) -> Result<i64, i64>
    requires amount >= 0

`ledger.find_balance` (`examples/banking_ledger.spx`)

@id("ledger.find_balance")
fn find_balance(left: Account, right: Account, wanted: i64) -> Option<i64>

`ledger.compound` (`examples/banking_ledger.spx`)

@id("ledger.compound")
fn compound(principal: i64, rate_percent: i64, years: i64) -> i64
    requires principal >= 0
    requires rate_percent >= 0
    requires rate_percent <= 100
    requires years >= 0
    requires years <= 10

`app.main` (`examples/banking_ledger.spx`)

@id("app.main")
fn main() -> i64

`byte.limit` (`examples/bytes_u8.spx`)

@id("byte.limit")
fn limit() -> u8

`byte.make` (`examples/bytes_u8.spx`)

@id("byte.make")
fn make(tag: u8) -> Sample

`byte.saturating_add` (`examples/bytes_u8.spx`)

@id("byte.saturating_add")
fn saturating_add(left: u8, right: u8) -> u8
    requires right <= limit()

`app.main` (`examples/bytes_u8.spx`)

@id("app.main")
fn main() -> i64

`calculator.add` (`examples/calculator.spx`)

@id("calculator.add")
fn add(left: i64, right: i64) -> i64

`calculator.subtract` (`examples/calculator.spx`)

@id("calculator.subtract")
fn subtract(left: i64, right: i64) -> i64

`calculator.multiply` (`examples/calculator.spx`)

@id("calculator.multiply")
fn multiply(left: i64, right: i64) -> i64

`calculator.divide` (`examples/calculator.spx`)

@id("calculator.divide")
fn divide(left: i64, right: i64) -> i64
    requires right != 0

`calculator.is-negative` (`examples/calculator.spx`)

@id("calculator.is-negative")
fn is_negative(value: i64) -> bool

`calculator.not` (`examples/calculator.spx`)

@id("calculator.not")
fn not(value: bool) -> bool

`app.main` (`examples/calculator.spx`)

@id("app.main")
fn main() -> i64

`glyph.initial` (`examples/chars.spx`)

@id("glyph.initial")
fn initial() -> char

`glyph.make` (`examples/chars.spx`)

@id("glyph.make")
fn make(symbol: char) -> Glyph

`glyph.order` (`examples/chars.spx`)

@id("glyph.order")
fn order(left: char, right: char) -> i64

`app.main` (`examples/chars.spx`)

@id("app.main")
fn main() -> i64

`example.main` (`examples/classes.spx`)

@id("example.main")
fn main() -> i64

`flow.choose` (`examples/control_flow.spx`)

@id("flow.choose")
fn choose(flag: bool, base: i64) -> i64

`app.main` (`examples/control_flow.spx`)

@id("app.main")
fn main() -> i64

`clock.logical_tick` (`examples/effects.spx`)

@id("clock.logical_tick")
fn logical_tick(value: i64) -> i64
    uses { clock.read }
    ensures result == value + 1

`app.main` (`examples/effects.spx`)

@id("app.main")
fn main() -> i64
    uses { clock.read }

`mut.accumulator` (`examples/explicit_mutation.spx`)

@id("mut.accumulator")
fn accumulator() -> i64

`mut.checked_steps` (`examples/explicit_mutation.spx`)

@id("mut.checked_steps")
fn checked_steps() -> i64

`main` (`examples/explicit_mutation.spx`)

@id("main")
fn main() -> i64

`expr.is_divide` (`examples/expression_evaluator.spx`)

@id("expr.is_divide")
fn is_divide(op: Op) -> bool

`expr.apply_unary` (`examples/expression_evaluator.spx`)

@id("expr.apply_unary")
fn apply_unary(value: i64, operation: UnaryOp) -> i64

`expr.evaluate` (`examples/expression_evaluator.spx`)

@id("expr.evaluate")
fn evaluate(pair: Pair, op: Op) -> i64

`expr.safe_divide` (`examples/expression_evaluator.spx`)

@id("expr.safe_divide")
fn safe_divide(left: i64, right: i64) -> Result<i64, i64>

`expr.safe_evaluate` (`examples/expression_evaluator.spx`)

@id("expr.safe_evaluate")
fn safe_evaluate(pair: Pair, op: Op) -> Result<i64, i64>

`expr.chain_scalars` (`examples/expression_evaluator.spx`)

@id("expr.chain_scalars")
fn chain_scalars(first: Pair, left_op: Op, second: Pair, right_op: Op, combine: Op) -> i64

`expr.fibonacci` (`examples/expression_evaluator.spx`)

@id("expr.fibonacci")
fn fibonacci(nth: i64) -> i64
    requires nth >= 0
    requires nth <= 20

`expr.fold_many` (`examples/expression_evaluator.spx`)

@id("expr.fold_many")
fn fold_many() -> i64

`app.main` (`examples/expression_evaluator.spx`)

@id("app.main")
fn main() -> i64

`fm.shift_x` (`examples/field_mutation.spx`)

@id("fm.shift_x")
fn shift_x(point: Point, step: i64) -> Point

`fm.track` (`examples/field_mutation.spx`)

@id("fm.track")
fn track(flag: bool) -> i64

`main` (`examples/field_mutation.spx`)

@id("main")
fn main() -> i64

`geometry.length_squared` (`examples/floats.spx`)

@id("geometry.length_squared")
fn length_squared(vector: Vector) -> f64

`geometry.inverse_length_squared` (`examples/floats.spx`)

@id("geometry.inverse_length_squared")
fn inverse_length_squared(vector: Vector) -> f64

`geometry.half` (`examples/floats.spx`)

@id("geometry.half")
fn half(value: f32) -> f32

`app.main` (`examples/floats.spx`)

@id("app.main")
fn main() -> i64

`app.http_router.byte_is` (`examples/http_app_routing.spx`)

serve_one, respond, and the send_* helpers below (past route_body_len) need these five tokens; every other function in this module is pure and declares no uses, exactly the posture documented for a route/handler in docs/HTTP-APPLICATION-ROUTING-V1.md.

@id("app.http_router.byte_is")
fn byte_is(view: borrow Slice<u8>, index: usize, expected: u8) -> bool

`app.http_router.lower` (`examples/http_app_routing.spx`)

@id("app.http_router.lower")
fn lower(byte: u8) -> u8

`app.http_router.find_from` (`examples/http_app_routing.spx`)

@id("app.http_router.find_from")
fn find_from(view: borrow Slice<u8>, start: usize, target: u8, limit: usize) -> usize
    ensures result <= limit

`app.http_router.find_blank_line` (`examples/http_app_routing.spx`)

The blank-line header terminator (\r\n\r\n), not merely the next \r: a request with more than one header line before the one a caller is scanning for needs the whole header block, not just its first line.

@id("app.http_router.find_blank_line")
fn find_blank_line(view: borrow Slice<u8>, start: usize, limit: usize) -> usize
    ensures result <= limit

`app.http_router.method_is_get` (`examples/http_app_routing.spx`)

@id("app.http_router.method_is_get")
fn method_is_get(view: borrow Slice<u8>) -> bool

`app.http_router.path_is_health` (`examples/http_app_routing.spx`)

@id("app.http_router.path_is_health")
fn path_is_health(view: borrow Slice<u8>, start: usize, end: usize) -> bool

`app.http_router.path_is_echo` (`examples/http_app_routing.spx`)

@id("app.http_router.path_is_echo")
fn path_is_echo(view: borrow Slice<u8>, start: usize, end: usize) -> bool

`app.http_router.header_name_is_content_length` (`examples/http_app_routing.spx`)

@id("app.http_router.header_name_is_content_length")
fn header_name_is_content_length(view: borrow Slice<u8>, index: usize, end: usize) -> bool

`app.http_router.skip_blanks` (`examples/http_app_routing.spx`)

@id("app.http_router.skip_blanks")
fn skip_blanks(view: borrow Slice<u8>, cursor: usize) -> usize
    ensures result >= cursor

`app.http_router.digit_value` (`examples/http_app_routing.spx`)

@id("app.http_router.digit_value")
fn digit_value(byte: u8) -> i64
    ensures result >= -1 && result <= 9

`app.http_router.decimal_at` (`examples/http_app_routing.spx`)

@id("app.http_router.decimal_at")
fn decimal_at(view: borrow Slice<u8>, start: usize) -> i64
    ensures result >= -1

`app.http_router.content_length_of` (`examples/http_app_routing.spx`)

@id("app.http_router.content_length_of")
fn content_length_of(view: borrow Slice<u8>, header_start: usize, header_end: usize) -> i64
    ensures result >= -1

`app.http_router.header_name_is_transfer_encoding` (`examples/http_app_routing.spx`)

A request declaring Transfer-Encoding is refused outright: this profile implements no chunked-body framing, so admitting the header — whether alone or alongside Content-Length — would let a request/response smuggling ambiguity through undetected (issue #189's "reject smuggling ambiguities such as conflicting Content-Length/transfer encoding"). Refusing the header unconditionally is the closed, fail-safe answer for a profile that never parses chunked framing at all, not only the narrower both-headers-present conflict case.

@id("app.http_router.header_name_is_transfer_encoding")
fn header_name_is_transfer_encoding(view: borrow Slice<u8>, index: usize, end: usize) -> bool

`app.http_router.has_transfer_encoding` (`examples/http_app_routing.spx`)

@id("app.http_router.has_transfer_encoding")
fn has_transfer_encoding(view: borrow Slice<u8>, header_start: usize, header_end: usize) -> bool

`app.http_router.request_has_smuggling_risk` (`examples/http_app_routing.spx`)

@id("app.http_router.request_has_smuggling_risk")
fn request_has_smuggling_risk(view: borrow Slice<u8>) -> bool

`app.http_router.route_for` (`examples/http_app_routing.spx`)

Route identity is a closed i64 domain, the same idiom std.net's wait_is_readable/wait_is_closed states use: 0 Health, 1 Echo, 2 NotFound, 3 MethodNotAllowed, 4 Malformed. A record or variant payload type-checks fine as a route/request/response shape (semaprax check verifies one in this profile's fixtures), but the bounded reference interpreter admits no record-field projection yet, so the profile's deterministic fixture lane below stays on the closed-domain idiom that every existing hosted profile (semaprax.network.v1, std.net) already uses, and that semaprax run (no --native build) executes end to end.

@id("app.http_router.route_for")
fn route_for(view: borrow Slice<u8>) -> i64
    ensures result >= 0 && result <= 4

`app.http_router.request_content_length` (`examples/http_app_routing.spx`)

@id("app.http_router.request_content_length")
fn request_content_length(view: borrow Slice<u8>) -> i64
    ensures result >= -1

`app.http_router.status_for` (`examples/http_app_routing.spx`)

@id("app.http_router.status_for")
fn status_for(route: i64) -> i64
    requires route >= 0 && route <= 4
    ensures result >= 100 && result <= 599

`app.http_router.body_len_for` (`examples/http_app_routing.spx`)

@id("app.http_router.body_len_for")
fn body_len_for(route: i64) -> usize
    requires route >= 0 && route <= 4

`app.http_router.route_status` (`examples/http_app_routing.spx`)

@id("app.http_router.route_status")
fn route_status(view: borrow Slice<u8>) -> i64

`app.http_router.route_body_len` (`examples/http_app_routing.spx`)

@id("app.http_router.route_body_len")
fn route_body_len(view: borrow Slice<u8>) -> usize

`app.http_router.send_health` (`examples/http_app_routing.spx`)

Everything above this line is pure: no uses. serve_one below is this profile's first server: it composes the already-implemented, already-hosted-green net_listen/net_accept/net_recv/net_send/ net_close/net_close_listener operations from Bounded Network Services v1 with the route table above into one accept/dispatch/respond/close lifecycle. It grants no ambient authority of its own — every operation it calls is already effect-gated by the module's own permit above.

@id("app.http_router.send_health")
fn send_health(peer: usize) -> usize
    uses { network.write }

`app.http_router.send_echo` (`examples/http_app_routing.spx`)

@id("app.http_router.send_echo")
fn send_echo(peer: usize) -> usize
    uses { network.write }

`app.http_router.send_not_found` (`examples/http_app_routing.spx`)

@id("app.http_router.send_not_found")
fn send_not_found(peer: usize) -> usize
    uses { network.write }

`app.http_router.send_method_not_allowed` (`examples/http_app_routing.spx`)

@id("app.http_router.send_method_not_allowed")
fn send_method_not_allowed(peer: usize) -> usize
    uses { network.write }

`app.http_router.send_malformed` (`examples/http_app_routing.spx`)

@id("app.http_router.send_malformed")
fn send_malformed(peer: usize) -> usize
    uses { network.write }

`app.http_router.respond` (`examples/http_app_routing.spx`)

Every arm returns the same Copy scalar (net_send's byte count), so this reuses the ordinary scalar-match idiom status_for/body_len_for already use above; a match arm that instead tried to build a typed Response aggregate here would be the exact SPX-T258 hostile case tests/http_app_routing.rs already exercises.

@id("app.http_router.respond")
fn respond(peer: usize, route: i64) -> usize
    uses { network.write }
    requires route >= 0 && route <= 4

`app.http_router.serve_one` (`examples/http_app_routing.spx`)

One accept/dispatch/respond/close lifecycle: bind, accept exactly one peer, read at most max_request bytes, route and respond, then release both the connection and the listener. The host that constructs the injected NetworkProvider — not this function — owns every socket, TLS, and credential decision; this function only ever sees the bounded handles Bounded Language Network I/O v1 and Bounded Network Services v1 already define. A caller that wants to keep serving calls this function again with a fresh listener; this slice does not add a persistent accept loop, graceful shutdown signal, or connection-limit counter, so it is not a claim of a production server lifecycle — see Non-claims.

@id("app.http_router.serve_one")
fn serve_one(bind_host: borrow Slice<u8>, port: usize, max_request: usize) -> bool
    uses { network.listen, network.accept, network.read, network.write, network.connect }

`app.http_router.serve_health_example` (`examples/http_app_routing.spx`)

A zero-argument, bool-returning entry point on a fixed illustrative loopback port: the exact shape semaprax::hosted_interpreter:: execute_network_command requires of a Language Network I/O v1 entry. tests/http_app_routing.rs runs this same source with only the port literal below substituted for an OS-assigned ephemeral one, against both a real loopback TcpNetworkProvider and a deterministic FixtureNetworkProvider, and asserts the two observations agree.

@id("app.http_router.serve_health_example")
fn serve_health_example() -> bool
    uses { network.listen, network.accept, network.read, network.write, network.connect }

`app.main` (`examples/http_app_routing.spx`)

@id("app.main")
fn main() -> i64

`example.main` (`examples/inheritance.spx`)

@id("example.main")
fn main() -> i64

`sum.pair` (`examples/integers_i32.spx`)

@id("sum.pair")
fn sum_pair(left: i32, right: i32) -> i32

`sum.checked` (`examples/integers_i32.spx`)

@id("sum.checked")
fn checked() -> i32

`compare.pair` (`examples/integers_i32.spx`)

@id("compare.pair")
fn compare(left: i32, right: i32) -> i64

`app.main` (`examples/integers_i32.spx`)

@id("app.main")
fn main() -> i64

`iterator.map` (`examples/iterator-operations.spx`)

@id("iterator.map")
fn map<T, U>(input: own Iter<T>, capacity: usize, transform: fn(T) -> U) -> Vec<U>

`iterator.filter` (`examples/iterator-operations.spx`)

@id("iterator.filter")
fn filter<T>(input: own Iter<T>, capacity: usize, keep: fn(T) -> bool) -> Vec<T>

`iterator.fold` (`examples/iterator-operations.spx`)

@id("iterator.fold")
fn fold<T, A>(input: own Iter<T>, initial: A, combine: fn(A, T) -> A) -> A

`iterator.map-via` (`examples/iterator-operations.spx`)

@id("iterator.map-via")
fn map_via<U, T>(input: own Iter<T>, capacity: usize, transform: fn(T) -> U) -> Vec<U>

`app.main` (`examples/iterator-operations.spx`)

@id("app.main")
fn main() -> i64

`lazy.first-if-step` (`examples/lazy-iterator-adapters.spx`)

@id("lazy.first-if-step")
fn first_if_step<T>(step: own IterStep<T>, keep: fn(T) -> bool) -> bool

`lazy.first-if` (`examples/lazy-iterator-adapters.spx`)

@id("lazy.first-if")
fn first_if<T>(input: own Iter<T>, keep: fn(T) -> bool) -> bool

`lazy.map-filter` (`examples/lazy-iterator-adapters.spx`)

@id("lazy.map-filter")
fn map_filter<T, U>(input: own Iter<T>, capacity: usize, transform: fn(T) -> U, keep: fn(U) -> bool) -> Vec<U>

`lazy.filter-fold` (`examples/lazy-iterator-adapters.spx`)

@id("lazy.filter-fold")
fn filter_fold<T, A>(input: own Iter<T>, keep: fn(T) -> bool, initial: A, combine: fn(A, T) -> A) -> A

`lazy.map-fold` (`examples/lazy-iterator-adapters.spx`)

@id("lazy.map-fold")
fn map_fold<T, U>(input: own Iter<T>, transform: fn(T) -> U, initial: U, combine: fn(U, U) -> U) -> U

`app.main` (`examples/lazy-iterator-adapters.spx`)

@id("app.main")
fn main() -> i64

`app.main` (`examples/lifecycle.spx`)

@id("app.main")
fn main() -> i64

`math.gcd` (`examples/math_algorithms.spx`)

@id("math.gcd")
fn gcd(left: i64, right: i64) -> i64
    requires left >= 0
    requires right >= 0
    ensures result >= 0

`math.lcm` (`examples/math_algorithms.spx`)

@id("math.lcm")
fn lcm(left: i64, right: i64) -> i64
    requires left > 0
    requires right > 0

`math.is_prime` (`examples/math_algorithms.spx`)

@id("math.is_prime")
fn is_prime(value: i64) -> bool
    requires value >= 0

`math.fibonacci` (`examples/math_algorithms.spx`)

@id("math.fibonacci")
fn fibonacci(nth: i64) -> i64
    requires nth >= 0
    requires nth <= 30

`math.factorial` (`examples/math_algorithms.spx`)

@id("math.factorial")
fn factorial(value: i64) -> i64
    requires value >= 0
    requires value <= 12

`math.digital_root` (`examples/math_algorithms.spx`)

@id("math.digital_root")
fn digital_root(value: i64) -> i64
    requires value >= 0

`app.main` (`examples/math_algorithms.spx`)

@id("app.main")
fn main() -> i64

`math.add` (`examples/meaning.spx`)

@id("math.add")
fn add(left: i64, right: i64) -> i64
    requires left >= 0
    requires right >= 0
    ensures result == left + right

`app.main` (`examples/meaning.spx`)

@id("app.main")
fn main() -> i64
    ensures result == 42

`example.token.identity` (`examples/native_callable.spx`)

@id("example.token.identity")
fn identity(value: own Token) -> Token

`app.main` (`examples/native_callable.spx`)

@id("app.main")
fn main() -> i64

`net-http-get.fetch` (`examples/net_http_get.spx`)

@id("net-http-get.fetch")
fn fetch() -> bool
    uses { network.connect, network.read, network.write, process.stdout.write }

`app.main` (`examples/net_http_get.spx`)

@id("app.main")
fn main() -> i64

`order.status_value` (`examples/order_lifecycle.spx`)

@id("order.status_value")
fn status_value(status: Status) -> i64

`order.is_terminal` (`examples/order_lifecycle.spx`)

@id("order.is_terminal")
fn is_terminal(status: Status) -> bool

`order.decide` (`examples/order_lifecycle.spx`)

@id("order.decide")
fn decide(line: Line, inventory: Inventory) -> Decision

`order.decision_value` (`examples/order_lifecycle.spx`)

@id("order.decision_value")
fn decision_value(decision: Decision) -> i64

`order.line_total` (`examples/order_lifecycle.spx`)

@id("order.line_total")
fn line_total(line: Line) -> i64

`order.process_steps` (`examples/order_lifecycle.spx`)

@id("order.process_steps")
fn process_steps(count: i64) -> i64

`order.apply_batch` (`examples/order_lifecycle.spx`)

@id("order.apply_batch")
fn apply_batch(total: i64, items: i64) -> i64

`app.main` (`examples/order_lifecycle.spx`)

@id("app.main")
fn main() -> i64

`order.safe_total` (`examples/order_lifecycle.spx`)

@id("order.safe_total")
fn safe_total(amount: i64) -> Result<i64, i64>

`buffer.inspect` (`examples/ownership.spx`)

@id("buffer.inspect")
fn inspect(buffer: borrow Buffer) -> i64

`buffer.consume` (`examples/ownership.spx`)

@id("buffer.consume")
fn consume(buffer: own Buffer) -> i64

`buffer.pipeline` (`examples/ownership.spx`)

@id("buffer.pipeline")
fn pipeline(buffer: own Buffer) -> i64
    ensures result == 2

`app.main` (`examples/ownership.spx`)

@id("app.main")
fn main() -> i64

`geometry.line.shift` (`examples/records.spx`)

@id("geometry.line.shift")
fn shift(line: Line, amount: i64) -> Line

`app.main` (`examples/records.spx`)

@id("app.main")
fn main() -> i64

`refutable.sign_class` (`examples/refutable_match.spx`)

@id("refutable.sign_class")
fn sign_class(value: i64) -> i64

`refutable.digit_name` (`examples/refutable_match.spx`)

@id("refutable.digit_name")
fn digit_name(digit: u8) -> i64

`refutable.route` (`examples/refutable_match.spx`)

@id("refutable.route")
fn route(code: char) -> i64

`main` (`examples/refutable_match.spx`)

@id("main")
fn main() -> i64

`ops.combine` (`examples/string_ops.spx`)

@id("ops.combine")
fn combine(left: string, right: string) -> string

`ops.world` (`examples/string_ops.spx`)

@id("ops.world")
fn world() -> string

`test.main` (`examples/string_ops.spx`)

@id("test.main")
fn main() -> i64

`ops.has_prefix` (`examples/string_ops_v2.spx`)

@id("ops.has_prefix")
fn has_prefix(value: string, prefix: string) -> bool

`ops.holds` (`examples/string_ops_v2.spx`)

@id("ops.holds")
fn holds(value: string) -> i64

`test.main` (`examples/string_ops_v2.spx`)

@id("test.main")
fn main() -> i64

`test.main` (`examples/strings.spx`)

@id("test.main")
fn main() -> i64

`text.count_byte` (`examples/text_analytics.spx`)

@id("text.count_byte")
fn count_byte(text: borrow str, target: u8) -> usize

`text.count_words` (`examples/text_analytics.spx`)

@id("text.count_words")
fn count_words(text: borrow str) -> usize

`text.is_empty_str` (`examples/text_analytics.spx`)

@id("text.is_empty_str")
fn is_empty_str(text: borrow str) -> bool

`text.starts_with_hello` (`examples/text_analytics.spx`)

@id("text.starts_with_hello")
fn starts_with_hello(text: string) -> bool

`text.contains_world` (`examples/text_analytics.spx`)

@id("text.contains_world")
fn contains_world(text: string) -> bool

`text.build_greeting` (`examples/text_analytics.spx`)

@id("text.build_greeting")
fn build_greeting(prefix: string, suffix: string) -> string

`text.palindrome_bytes` (`examples/text_analytics.spx`)

@id("text.palindrome_bytes")
fn palindrome_bytes(text: string) -> bool

`app.main` (`examples/text_analytics.spx`)

@id("app.main")
fn main() -> i64

`example.usize.checksum` (`examples/useful_data_usize_v1.spx`)

@id("example.usize.checksum")
fn checksum(seed: usize, count: usize) -> usize

`app.main` (`examples/useful_data_usize_v1.spx`)

@id("app.main")
fn main() -> i64

`loops.digit_sum` (`examples/while_loops.spx`)

@id("loops.digit_sum")
fn digit_sum(value: i64) -> i64

`loops.factorial` (`examples/while_loops.spx`)

@id("loops.factorial")
fn factorial(value: i64) -> i64

`app.main` (`examples/while_loops.spx`)

@id("app.main")
fn main() -> i64