The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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