New answers tagged proof-assistants
1
I’m not sure I get what you are trying to do – or, rather, how your example corresponds to your goal. Indeed, in your code you postulate those three types a, b and c, but these are not really "arbitrary terms", rather they are types (this is just what you have postulated!). If you wanted to work with unspecified carriers, what you could do instead ...
Top 50 recent answers are included