The Coq mailing list

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

It seems like a version incompatibility though, doesn't it?

Now I must use ugly syntax like the  following:

 

Eval simpl in texpDenote _ (TNConst 42).
Eval simpl in texpDenote _ (TBConst true).
Eval simpl in texpDenote _ (TBinop _ _ _ TTimes (TBinop _ _ _ TPlus (TNConst 2)(TNConst 2))(TNConst 7)).
Eval simpl in texpDenote _ (TBinop _ _ _ (TEq Nat) (TBinop _ _ _ TPlus (TNConst 2) (TNConst 2))(TNConst 7)).
Eval simpl in texpDenote _ (TBinop _ _ _ TLt (TBinop _ _ _ TPlus (TNConst 2) (TNConst 2))(TNConst 7)).

 

I remember I executed parts of CPDT before and most things worked.

On Mon, Oct 17, 2016 at 4:43 PM, Satrajit Roy <satrajit.roy AT gmail.com> wrote:

Ahhh!!! Thank you so much!!

On Mon, Oct 17, 2016 at 4:18 PM, John Wiegley <johnw AT newartisans.com> wrote:

>>>>> "SR" == Satrajit Roy <satrajit.roy AT gmail.com> writes:

SR> My exposure to COQ is limited; so I'm possibly not seeing something
SR> obvious. Given the following definitions, why isn't the last one working?

After a few changes, this works. What you wrote failed to type check, not
because of the TNConst case, but because the type of the term you were
creating in the TBinop case was not the correct type, and this affected the
type expected for the TNConst case.

--8<---------------cut here---------------start------------->8---
Require Import Bool.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 t2 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=> tbinopDenote _ _ _ b (texpDenote _ e1) (texpDenote _ e2)
  end.
--8<---------------cut here---------------end--------------->8---

--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2

--

Satrajit

--

Satrajit