Module spec/refine
spec/refine
Types
Refine
type-function
fn(comptime(T) : Type) -> (comptime(fn_return_yo9dc7b15e_id_18) : Type)
A value of type T paired with a (compile-time) refinement
predicate. Phase 0 ignores the predicate; later phases will
require it as a second parameter and enforce it via
the SMT backend.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
NonZero
type-function
fn(comptime(T) : Type) -> (comptime(fn_return_yo9dc7b15e_id_37) : Type)
NonZero(T) — values of T that are not zero. Phase 0 is a
type alias for T; future phases will enforce via verification.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Bounded
type-function
fn(comptime(T) : Type, comptime(_lo) : T, comptime(_hi) : T) -> (comptime(fn_return_yo9dc7b15e_id_64) : Type)
Bounded(T, lo, hi) — values of T in the closed range
[lo, hi]. Phase 0 is a type alias for T. T must be Comptime
so the bounds can be compile-time-known.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
_lo | T | comptime |
_hi | T | comptime |