3 ms·
Well you can encode any logic you want in dependent types, so yeah probably!
by agentultra 3y ago
Well you can encode any logic you want in dependent types, so yeah probably!
- practal 3y agoFair enough. Although to encode a proposition as a type, only to then view it as a proposition again, would be two wrappers too many for my taste. I prefer to keep the notions of truth and types apart. In practice, this makes the logic both simpler and more expressive.