Module types 

Auto-generated module

🤖 Generated with SplitRS

Structs

DedekindCutQ

A Dedekind cut representation over the rationals (using integer pairs p/q).

FiniteLinearOrder

A finite linear order (totally ordered finite set).

FinitePartialOrder

A partial order on a finite set, stored as an adjacency matrix.

OrderedRange

A range structure for ordered types.

OrderedTable

A simple table that maps keys to values, sorted by a comparison function.

OrderingBuilder

A builder that accumulates multiple comparison results and returns the first non-Equal one.

OrdinalCnf

Represents an ordinal in Cantor Normal Form.

WqoInstance

Represents a well-quasi-order (WQO) over a finite carrier.

Enums

Ordering

A Lean 4-style ordering value (mirrors Ordering in the kernel env).