The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!