just did a map using two lists as input! logic programming is cooool
having fun playing with makam:
Conversation
Having too much fun with Makam…
3
3
Now playing with some declarative typing rules for Martin-Löf type theory in Makam! Finally starting to get my head around why they are defined the way they are, I think? Not sure if I want to use explicit substitutions yet, hence the commented out declarations… 🤔
Replying to
I'm _thinking_ that these general rules mean that you don't have to write as many duplicated rules for things like booleans. For example if we write an elimination rule with the eliminator on the left, we get the one on the right for free, thanks to the symmetry rules:
1
As somebody who often reads type theory papers and books by trying to get as quickly to "how do I implement this?" as possible, this is a rather cool way to think about stuff, even if it's a bit weird and different!
2