The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thank you.

I also realized, another solution to see the "functional" rather than "tactical" view is to just "Set Printing All. Print extract_valueT." :-)

On Sun, Aug 25, 2013 at 9:58 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

On Sunday, August 25, 2013 09:39:52 PM t x wrote:
> Hi,
>
> In the follow code example:
>
> https://gist.github.com/anonymous/6336486
>
> How do I rewrite extract_valueT as extract_valueT' through the use of match?
>
> In particular, I don't know how to use the "rewrite H" for the types.
>
> (I prefer style 2 as it's easier to read, even if a bit more involved to
> write.)

How about:

  Definition extract_valueT' (v: PrimValue)
                             (T: Type)
                             (H: type_of v = T) : T :=

    eq_rect _ (fun A:Type => A) (extract_value v) _ H.

or pretty much equivalently:

  Definition extract_valueT'' (v: PrimValue)
                              (T: Type)
                              (H: type_of v = T) : T :=
    match H in (_ = T) return T with
    | eq_refl => extract_value v
    end.
--
Daniel Schepler