The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  Here is my min fail case.

Require Import ZArith Omega.
Local Open Scope Z_scope.

Record Foo :=
  { n : Z;
    H : n < 10 }.


Lemma lem__5_lt_10: 5 < 10.
Proof. omega. Qed.


(* this line works *)
Definition a := Build_Foo 5 lem__5_lt_10.


(* this line does not work *)
Definition a' := Build_Foo 5 _.

(*  Question: is there a way to use Program / refine
    so that I can write the above?

In particular, I want to:
  * fill in the proof after the "Build_Foo"

I do NOT want to:
  * define a lemma before hand to use.

 *)

  Is the above possible?

Thanks!