coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] co-defining an Inducive + a Fixpoint

From: t x <txrev319 AT gmail.com>
To: Rui Baptista <rpgcbaptista AT gmail.com>
Cc: Jason Gross <jasongross9 AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] co-defining an Inducive + a Fixpoint
Date: Thu, 29 Aug 2013 22:38:38 +0000

Jason: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq agrees with you.

Rui: interesting, I think this suffices.

On Thu, Aug 29, 2013 at 9:43 PM, Rui Baptista <rpgcbaptista AT gmail.com> wrote:

What about:

Inductive Foo' :=
| fooA (n: nat)
| fooPlus (f1: Foo') (f2: Foo')
| fooWeird (f1: Foo') (f2: Foo') (f3: Foo').

Fixpoint evalFoo f :=
match f with
| fooA n => n
| fooPlus f1 f2 => (evalFoo f1 ) + (evalFoo f2)
| fooWeird f1 f2 f3 => (evalFoo f1) + (evalFoo f2) + (evalFoo f3)
end.

Definition Foo :=
{f1 : Foo' | forall f2 f3 f4, f1 = fooWeird f2 f3 f4 -> evalFoo f4 = 10}.

[Coq-Club] co-defining an Inducive + a Fixpoint, t x, 08/29/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Jason Gross, 08/29/2013
  - Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Rui Baptista, 08/29/2013
    - Re: [Coq-Club] co-defining an Inducive + a Fixpoint, t x, 08/30/2013
      - Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Andrew Cave, 08/30/2013