The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

What you probably want is something with a sigma type in the positive position, for which you can use refine, since you're working with a logical term:

Definition pair_fun_template : forall (p : nat * nat), {k | k = fst p}.

   refine (fun p => match p with pair t u => (exist _ _ _) end); crush.

Defined.

Kris

On Wed, Sep 4, 2013 at 9:29 AM, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

(1) I know that I can take advantage of partial proofs using refine, but can I treat partial proofs as first class values? E.g., I'm trying to do this, but Coq complains that it can't infer the value of the hole.

Definition pair_fun_template: pair_nat_nat -> nat :=

(fun p: pair_nat_nat => 

    match p with mk_pair t u => (_ : nat) end).

(2) When using CoqIDE and literate Coq in the style of Pierce's book, Coq constantly complains, "Warning: query commands should not be inserted in scripts." How can I turn off these warnings?

Thanks!

Kevin