Types with Predicates
← Back to Refinement Types
Types constrained by logical predicates that restrict the set of valid values. For example, { x: Int | x > 0 } represents positive integers. Refinement types can verify properties like non-emptiness, bounds, and sortedness at compile time using SMT solvers.