I am trying to define a logical calculus using one data type for the rules.
There are three types of rules and each has 0,1 or 2 assumptions (rule,
rule1 and rule2 below). I have defined all the rules as different
constructors so the difference between the types according to 0,1 or 2
assumptions is very weak. I would still like to be able to group the rules
in types according to the number of assumptions in order to use pattern
matching. Is there a simple way to do that or another way I should implement
the data type such that I can refer to the rules both according to their
number of assumptions and according to their type?
> One beginner to another, what about just breaking down and using multiple
> data declarations, then packing the rules into the outer data type and the
> misc. parameters into the inner data type?:
> data RuleBox = Rule0 RuleZero | Rule1 RuleOne Rule | Rule2 RuleTwo Rule
> data RuleZero = Axiom Sequent
> data RuleOne = WeakeningL Sequent FormulaOccur | WeakeningR Sequent
> FormulaOccur | ContractionL ... | Contraction R ... | PermutationL ... |
> PermutationR ... | NotL ... | NotR ...
> data RuleTwo = Mix Sequent FormulaOccur | AndL ... | AndR ...