The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Marco,

Have you tried something using a [return] in your [match]?
Something similar to this should work:

===================================
Variable A : Type.

Definition f (optA : option A) :=
(match optA as x return optA = x -> nat with
  | Some a => (fun p => O)
  | None => (fun p => 1)
end) (eq_refl optA).
===================================

Cheers,

--
guillaume



On 13 July 2011 14:21, Marco Servetto 
<marco.servetto AT gmail.com>
 wrote:
> Hi, thanks for the fast reply,
> No, I'm not defining a tactique.
> Definition f optA:=
>  match optA with
>   |Some a=>Some ( g a (p:(Some a=optA))
>  |None=>None
>   end.
> g is a type constructor of a record with some constraint, like
> in
> Record G:Type
> := g {
>  data: ...;
>  constraint: true=... data ...
>  }.
>
> f is a function that takes an a:G and produces an a0:G if is possible.
> Here I have omitted all the computation.
>