The Coq mailing list

[Christian Kjær Larsen <christianden AT gmail.com>]

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