Enumerates the closed HOL terms needed for γ-finite instantiation and primitive substitution.
gen_o/1 produces every ground term of a given propositional type — truth
values at o, the four unary connectives at o → o, the sixteen binary
connectives at o → o → o, and higher-arity Boolean functions via
if-then-else expansion. Results are memoised per-process; the same lookup
from a worker is a cache hit.
Summary
Functions
Enumerates all closed terms of the given propositional type.
Functions
@spec gen_o(o_type()) :: Enumerable.t(ShotDs.Data.Term.term_id())
Enumerates all closed terms of the given propositional type.
Results are memoized per-process after the first call. Covers truth values
(o), unary connectives (o → o), binary connectives (o → o → o), and
general finite Boolean functions of higher arities via if-then-else expansion.