The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

The variable x depends on t, so when you match on t if you want to use x 
at a type depending on the branch you have to do a commutative cut

Definition liftVal t : tyDenote t -> exp t :=
  match t with
  | Nat => fun x => NatLit x
  | Nat' => fun x => Nat'Lit x
  | Bool => fun x => BoolLit x
  end.

Gaëtan Gilbert

On 22/03/2019 09:17, Christian Kjær Larsen wrote:
> Hi,
>
> I have some GADT for expressions, and I want to lift values into 
> expressions like this
>
> Inductive ty : Set :=
> | Nat  : ty
> | Nat' : ty
> | Bool : ty.
>
> Definition tyDenote (t : ty) : Set :=
>    match t with
>    | Nat  => nat
>    | Nat' => nat
>    | Bool => bool
>    end.
>
> Inductive exp : ty -> Set :=
> | NatLit : nat -> exp Nat
> | Nat'Lit : nat -> exp Nat'
> | BoolLit : bool -> exp Bool.
>
> Definition liftVal t (x : tyDenote t) : exp t :=
>    match t in ty return exp t with
>    | Nat => NatLit x
>    | Nat' => Nat'Lit x
>    | Bool => BoolLit x
>    end.
>
> But the last definition will not type check. Do any of you know how to 
> write a function like this? One complication is probably that different 
> object level types have the same denotation.
>
> Cheers,
> Christian