The Coq mailing list

[Damien Andrew Tamburri <maelstrom_dat AT hotmail.com>]

Hello CoqClubbers!

    I am having difficulty in including the context for rules in Natural Deduction, within a structure representing Natural Deduction Trees themselves (see attached file).. I keep getting the "The term "In a X" has type "Prop" which is not a (co-)inductive type." error for the last three constructors of type NDTree.. can anyone explain me if and how I can use the construct "if..then..else" in this way? what other context alternatives are there?

      many thanks!

        Damian Andrew Tamburri

---

Click less, mail more: Hotmail on the new MSN homepage!

Attachment: project.v
Description: Binary data