The Coq mailing list

[Satrajit Roy <satrajit.roy AT gmail.com>]

My exposure to COQ is limited; so I'm possibly not seeing something obvious.

Given the following definitions, why isn't the last one working?

Require Import Bool Arith List.

 

Inductive type:Set:=Nat|Bool.

Inductive tbinop:type->type->type->Set:=
  |TPlus:tbinop Nat Nat Nat
  |TTimes:tbinop Nat Nat Nat
  |TEq:forall t, tbinop t t Bool
  |Tlt:tbinop Nat Nat Bool.

Inductive texp:type->Set:=
  |TNConst:nat->texp Nat
  |TBConst:bool->texp Bool
  |TBinop:forall t1 t2 t, tbinop t1 t1 t->texp t1->texp t2->texp t.

 

Definition typeDenote(t:type):Set:=
  match t with
    |Nat=>nat
    |Bool=>bool
  end.

 

Definition tbinopDenote arg1 arg2 res(b:tbinop arg1 arg2 res):typeDenote arg1->typeDenote arg2->typeDenote res:=
  match b with
    |TPlus=>plus
    |TTimes=>mult
    |TEq Nat=>beq_nat
    |TEq Bool=>eqb
    |TLt=>leb
  end.

 

Fixpoint texpDenote t (e:texp t):typeDenote t:=
  match e with
    |TNConst n=>n
    |TBConst b=>b
    |TBinop _ _ _ b e1 e2=>(tbinop b)(texpDenote e1)(texpDenote e2)
  end.

 

​Error:
In environment
texpDenote : forall t : type, texp t -> typeDenote t
t : type
e : texp t
n : nat
The term "n" has type "nat" while it is expected to have type
 "typeDenote ?t@{t1:=Nat}".
​

 

--

Satrajit