dealt with infix notation in a less aggressive way, cannot display infix as it is, though at least now prettyprint can feedback to parser without error.
fix a nasty bug of not updating the local etype when done with solving a formula
add a module for sums
manually deriving ind is nuts, let's do automatic deriving.
handling comprehension.
add some exercise on infinite data structure.
support a more clean view on deriving inductive set
implement automatic deriving induction for all inductive type
add ind.hs
finished initial versio of automatic deriving induction
add keyword Ind
add native iftheelse support
implimented the pattern matching compiler
bind pattern compiler to preprocess
the mixture rule is not corret, this kind of bug are deadly serious, do that tomorrow
fixed the big bug, now still the naming policy is confusing.
confirm that it is a bug in spj's book, so the implementation is correct as far as I can tell
add a test file for pattern matching desugaring
add a test file for automatically deriving induction principle
merge the pattern matching branch.