The Coq mailing list

[Dan Frumin <dfrumin AT cs.ru.nl>]

Dear Satrajit,

Perhaps it would help do declare all the arguments representing types
in your functions as implicit. For instance:

```
Arguments texpDenote {t} e.
Arguments TBinop {t1 t2 t} op a1 a2.
Eval simpl in texpDenote (TNConst 42).
Eval simpl in texpDenote (TBinop TTimes (TNConst 42) (TNConst 2)).
```

Alternatively you can define ceratin arguments as implicit directly when 
defining your function.
For instance:

```
Fixpoint texpDenote {t} (e:texp t):typeDenote t:=
 match e with
   |TNConst n=>n
   |TBConst b=>b
   |TBinop r1 r2 r b e1 e2=>
    tbinopDenote r1 r2 r b (texpDenote e1) (texpDenote e2)
 end.
Eval simpl in texpDenote (TNConst 42).
```

Kind regards, 
- Dan

On 10/18, Satrajit Roy wrote:
> 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