Hello,

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?

27 data Rule = Axiom {lowseq :: Sequent}

28 | WeakeningL {rule :: Rule, lowseq :: Sequent, foccur ::

FormulaOccur}

29 | WeakeningR {rule :: Rule, lowseq :: Sequent, foccur ::

FormulaOccur}

30 | ContractionL {rule :: Rule, lowseq :: Sequent, foccur ::

FormulaOccur}

31 | ContractionR {rule :: Rule, lowseq :: Sequent, foccur ::

FormulaOccur}

32 | PermutationL {rule :: Rule, lowseq :: Sequent}

33 | PermutationR {rule :: Rule, lowseq :: Sequent}

34 | Mix {rule1 :: Rule, rule2 :: Rule, lowseq :: Sequent, foccur

:: FormulaOccur}

35 | NotL {rule :: Rule, lowseq :: Sequent, foccur ::

FormulaOccur}

36 | NotR {rule :: Rule, lowseq :: Sequent, foccur ::

FormulaOccur}

37 | AndL {rule1 :: Rule, rule2 :: Rule, lowseq :: Sequent, foccur

:: FormulaOccur}

38 | AndR {rule1 :: Rule, rule2 :: Rule, lowseq :: Sequent, foccur

:: FormulaOccur}

39 deriving (Eq, Show)

Thanks,

Tomer

-------------- next part --------------

An HTML attachment was scrubbed...

URL:

http://www.haskell.org/pipermail/beginners/attachments/20090111/7bee0003/attachment.htm