Standard Library
Self-hosted in Cure, extracted live from lib/std/
at compile time. 68 modules total.
Core & Type System
Std.Core
Identity, composition, booleans, comparison, and the `Result` / `Option` sum types.
Std.Decision
Decidable propositions -- a definitive yes-or-no answer that carries its own evidence.
Std.Dynamic
A typed, honest stand-in for a dynamically-shaped value — the well-typed replacement for `Any`.
Std.Literal
User-defined contextual integer literals.
Std.Match
Convenience helpers built on top of v0.18.0 deep destructuring.
Std.Optic
Statically-typed optics: lenses, affine traversals, and traversals.
Std.Refine
Refinement-oriented proof helpers for numeric predicates. Prefer ordinary indexed data and explicit propositions for new APIs; this module remains for compatibility with existing refinement clients.
Std.Sigma
The dependent pair (Σ-type) — `Sigma(a, b)` packages a value `x : a` together with a value of type `b(x)`, where the second component's type may depend on the first. This is the library inductive that the compiler wires the surface sugar to: `%[x, y]` builds one, `.1`/`.2` project, and `Sigma(x: T, U)` is the type syntax (spec 2026-07-09-sigma-retirement).
Std.Telescope
The telescope type — the shape all surface tuples are made of.
Primitive Types
Std.Atom
The primitive interned symbol.
Std.Binary
The bridge between Cure's two string representations.
Std.Bool
Booleans as a real inductive type.
Std.Char
The Unicode code point — Cure's character type.
Std.String
Value-surface string operations: length, concat, split, trim, case conversion, and integer/float/atom parsing.
Std.Tuple
`use Std.Sigma` supplies the projection globals `.1`/`.2`/`.i` lower to (`sigma_first`, `sigma_second`, `tproj2`…`tproj8`). Every ordinary module receives those ambiently — `Std.Sigma` is a whole-module `@prelude` — but `@prelude opaque type Tuple` below puts THIS module in the prelude-bootstrap closure, and a bootstrap module is elaborated with no prelude of its own so it cannot be injected back into one of its own dependencies. The import must therefore be explicit. `Std.Sigma` imports nothing, so this adds no cycle.
Std.Unit
The unit type — exactly one value, carrying no information.
Numeric & Math
Std.Arithmetic
Arithmetic interfaces, split by operation rather than one monolithic `Num` (spec §2.3): motivated by `Std.Measurements` (`Duration` has `add`/`sub`/`scale` but no `Duration * Duration` — measurements.cure:84-90).
Std.Bounded
Bounded natural indices.
Std.Decimal
Arbitrary-precision decimal arithmetic.
Std.Float
The primitive machine floating-point number.
Std.Int
Canonical inductive integer, native at runtime.
Std.Math
Mathematical operations.
Std.Measurements
Literal units of measure (design 2026-07-08-units-macro-design).
Std.Nat
Peano natural numbers for type-level computation.
Collections & Iteration
Std.Data.Suffix
A proof that `rem` is a suffix of `orig`, indexed by whether at least one element was consumed. This is the foundation of total lexers and parsers: recursive drivers may descend only after receiving a `Consumed(..., True, ...)` witness.
Std.Iter
Lazy iterators.
Std.List
Eager, persistent, singly-linked lists.
Std.Map
Map operations: get, put, delete, keys, values, merge.
Std.NonEmpty
A list that is *guaranteed* to hold at least one element.
Std.Set
Sets represented as maps with `true` values.
Std.Vector
Length-indexed vectors.
Protocols & Abstractions
Std.Comparable
`use Std.Bool` supplies `` `not` `` for the derived `` `<=` ``/`` `>=` ``; `use Std.Equatable` provides the `Equatable(t)` superinterface required by `Comparable(t)`.
Std.Equatable
`use Std.Bool` supplies `` `not` `` for the derived `` `!=` ``.
Std.Equivalent
Propositional equality — the inductive identity type `Equivalent(a, x, y)` (spec 2026-07-04-identity-type-as-inductive).
Std.Functor
Functor interface for structures that support `fmap`.
Std.Operators
Prelude fixity declarations for Cure's built-in operators. This module is loaded automatically; it does not expose a runtime API.
Std.Semigroup
Semigroup interface — types that support an associative `combine`.
Std.Show
The `Show` protocol: convert values to their human-readable `String` form.
Control & Error Handling
Concurrency & OTP
Std.Actor
The structured actor surface is a source-defined family.
Std.ActorBehavior
Shared compile-time substrate for actor-like abstractions. Both public `actor` declarations and constrained actors such as `fsm` supply ordinary checked declarations here; this function emits the final direct BEAM behaviour module without introducing a runtime container or dispatcher.
Std.App
The structured application surface is source-defined.
Std.Beam
Opaque native term at the foreign boundary. It can be passed to trusted primitives, but ordinary Cure code cannot inspect it or claim a type for it.
Std.CRDT
Conflict-free Replicated Data Types for Cure (v0.27.0).
Std.ExitReason
Typed reasons understood by Cure's safe process APIs. `Because` is the deliberate raw-atom escape hatch for application- and OTP-specific reasons; callers do not need to abandon the typed API to use one.
Std.Fsm
The structured FSM surface reuses the generic family parser.
Std.Otp
Public names for the sealed raw carriers used by this module's signatures. These aliases make the `Std.Otp` interface self-contained without leaking every bare name imported from `Std.Otp.Raw` into downstream modules.
Std.Otp.Raw
SEALED unsafe raw base for the typed BEAM process algebra.
Std.Process
Compatibility façade for process-signal operations.
Std.Supervisor
The structured supervisor surface is source-defined.
System & I/O
Syntax & Metaprogramming
Std.Syntax
The generic quoted-AST value a Tier-3 `computed by` elab receives and returns (macro-facility design §3, generic layer). Reflects the parser's `{tag, meta, third}` node: `Node` for a child list, `Leaf` for a scalar third value, `Raw` for a node the parser produced that doesn't fit the `{tag, meta, third}` shape at all (e.g. a bare `impossible`-body marker or a non-conforming pattern tuple) -- reflected opaquely rather than crashing. `attrs` carries the semantic meta (a function's name, an operator, a literal's subtype) — dropping it would lose those. A meta value need not be a plain scalar: `SynLit` also covers a list of values (`SList`), a nested AST (`SSyntax`), and a lookup table (`SMap`), each losslessly. Source positions are not represented (the expansion is re-elaborated, K3 firewall).
Std.Syntax.Raw
Explicitly unsafe syntax construction.
Proofs & Formal Verification
Std.Proof
Genuine propositional-equality proofs over the inductive `Std.Nat` (spec 2026-07-04-identity-type-as-inductive).
Std.Proof.BooleanReflection
Boolean-connective algebra over `IsTrue` (constructive, zero trust).
Std.ProofDirectedExtraction
A deliberately small proof-directed data pipeline.
Std.Proof.IntDiscrete
Discreteness of the inductive integers: strict comparison against `right` is the same Boolean proposition as non-strict comparison against `right-1`.
Std.Proof.IntMath
Proof-carrying facts about `Int`, via decidable-Boolean reflection.
Std.Proof.IntOrder
Proof-carrying order on the inductive integers `Int = FromNat(Nat) | NegativeSuccessor(Nat)`, via decidable-Boolean reflection.
Std.Proof.LinearArithmetic
Executable affine syntax for verified LIA reflection. This module is total and deliberately rejects malformed dimensions instead of inheriting List.zip_with's truncating semantics.
Std.Proof.LinearArithmetic.Semantics
Trusted semantic lemmas used by the linear-arithmetic proof modules. The declarations relate coefficient lists and their evaluated sums.
Std.Proof.Math
Proof-carrying mathematics used by refinements and ordinary Cure programs.