5 ms·
You are talking about dependent types (https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type) and only a few theorem-proving
by infinite8s 11y ago
You are talking about dependent types (https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type) and only a few theorem-proving languages support them.