Module spec/refine
spec/refine
Types
Refine
type-function
fn(T : Type) -> 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(T : Type) -> 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(T : Type, _lo : T : (Comptime), _hi : T) -> 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) | comptime |
_hi | T : (Comptime) | comptime |
NonEmpty
type-function
fn(T : Type) -> Type
NonEmpty(T) — collection types with at least one element.
Phase 0 is a type alias for T.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |