In natural deduction, is there a word for a bunch of related formation, introduction, elimination, and computation rules? Examples would be: pairs, functions, records, etc. I think some would call these 'types' but somehow I feel that only covers the type constructor part.
Conversation
Replying to
Yeah I think it's a similar problem here: twitter.com/brendanzab/sta - like, I want to talk about specific 'language feature', like the function arrow+lambda+application+beta reduction together as a single thing.
Quote Tweet
Replying to @JohnMeuser
Doesn't 'framework' refer to the collection of different features however? Or are you talking about having a framework that has only a 'pair' defined, and 'function' defined, then somehow smooshing them together to form another, larger framework?
So I guess I could maybe say 'the function theory' and the 'record theory'?