just did a map using two lists as input! logic programming is cooool
having fun playing with makam:
Conversation
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… 🤔
1
1
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
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
feed in two lists and get a sort of `zip_with` predicate :)
compare `eval` with `equal` for `array_intro`s here:
1
Replying to
How is your experience using makam so far? Does it feel polished/feature complete? How is the dev experience?
1
Pretty good! There's quite a bit of polish that needs to be done - but it's definitely usable and the author is pretty responsive on the issue tracker and on email. Some of the main issues are the limited docs, and poor error reporting (only one error reported at a time).
1
Show replies