4 ms·
These are called refinement types (https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type). Provable termination isn’t str
by layer8 1y ago
These are called refinement types (https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type).
Provable termination isn’t strictly necessary I think, because compile-time evaluation, or metaprogramming in general, is usually Turing-complete anyway.