The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I believe this is called induction-recursion, and I believe that agda supports it, while coq does not.  You could try implementing it in OCaml and asking the coq-devs to merge your branch, though that might be quite an undertaking.

I don't know of any work-arounds, though I haven't explored it much.

-Jason

On Aug 29, 2013 4:48 PM, "t x" <txrev319 AT gmail.com> wrote:

Hi,

  Here is my minimal failure case: https://gist.github.com/anonymous/6383213

  What I want is to simultaneouly define "Inductive Foo: Set" and "Fixpoint evalFoo: Foo -> nat"

  such that the Inductive can have a term that involves evalFoo (in particular, a proof that evalFoo gets a certain value).

Can I do this in Coq? (If so, how, if not, what is the closest alternative).

Thanks!