The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

>> I could have something like:
>> Inductive data_prop ...
>> ...
>> ...
>> with Fixpoint func (data_prop).
> 
> Hi Dimitry, what would this look like without the '...'s?
> 

It would look like an inductive definition of data_prop as written in
previous posts accompanied by a definition of the fixpoint func that uses
subterms of data_prop. But forget about it. As mentioned by Adam Chlipala
above, it is not supported in Coq. 
-- 
View this message in context: 
http://www.nabble.com/Data-Structures-tp22535211p22568059.html
Sent from the Coq mailing list archive at Nabble.com.