Loading ...
Sorry, an error occurred while loading the content.

OCaml and Coq tactics

Expand Messages
  • Marko Malikoviæ
    Greetings, I m new on this list and didn t learn OCaml yet. The reason why I m here is that one Coq tactic is missing for my needs. So, my questions are: 1.
    Message 1 of 2 , Apr 7, 2008
    • 0 Attachment
      Greetings,

      I'm new on this list and didn't learn OCaml yet. The reason why I'm here is that one Coq tactic is missing for my needs.
      So, my questions are:

      1. Somebody use Coq on this list?
      2. Do you think I can write new tactic in Objective Caml which will allow me to compare hypotheses with the same ident over different subgoals and will allow me to do "something" if all hypotheses have equal values and "something else" if all hypotheses haven't equal values? So, can I surmount a independents of subgoals? I don't like to spend a time to learn OCaml for nothing:)

      Example is:

      Subgoal 1:

      H : x=value_1

      Subgoal 2:

      H : x=value_2
      ...

      Subgoal n:

      H : x=value_n

      So, I need tactic (or tactical) which will apply one tactic if value_1, value_2,..., value_n are equal in all subgoals, but will apply another tactic if value_1, value_2,..., value_n are not equal.

      Thanks you very much for your help or for your opinion,
      Greetins from Croatia,
      Marko Malikovi�


      ____________________________________________________________________________________
      You rock. That's why Blockbuster's offering you one month of Blockbuster Total Access, No Cost.
      http://tc.deals.yahoo.com/tc/blockbuster/text5.com

      [Non-text portions of this message have been removed]
    • Richard Jones
      Coq has a mailing list and I think you ll get much better answers by posting your question there: http://pauillac.inria.fr/pipermail/coq-club/ Rich. -- Richard
      Message 2 of 2 , Apr 7, 2008
      • 0 Attachment
        Coq has a mailing list and I think you'll get much better answers by
        posting your question there:

        http://pauillac.inria.fr/pipermail/coq-club/

        Rich.

        --
        Richard Jones
        Red Hat
      Your message has been successfully submitted and would be delivered to recipients shortly.