Refinement

Common, executable refinement predicates. Import qualified (for example, ``Refinement.non_negative n``) or ``open Refinement`` deliberately.

Table of Contents

Functions

def non_negative (n : Int) : Bool

def positive (n : Int) : Bool

def non_positive (n : Int) : Bool

def negative (n : Int) : Bool

def in_range (lo : Int) (hi : Int) (n : Int) : Bool

def bounded (lo : Int) (hi : Int) (n : Int) : Bool

Solver-friendly names for the most common collection refinements.

def non_empty_size (size : Int) : Bool

def valid_index (size : Int) (index : Int) : Bool

Float counterparts use explicit names rather than ad-hoc overloads, keeping predicate lookup predictable across the single Aeon value namespace.

def non_negative_float (n : Float) : Bool

def positive_float (n : Float) : Bool

def unit_interval_float (n : Float) : Bool