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
the ones you described are all the result of embedding some algebraic laws into the rules, right? i wonder if universal algebra is a useful frame here
1
1
what does plt redex call them internally, if anything?
1
Replying to
Hmm not sure - I didn't think redex forced you to split things up into formation, introduction, elimination, and computation rules. ie. I thought all it cared about was judgement forms and rules, but I could be remembering incorrectly… 😅