The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

> Any neat way to side-step this limitation?

Hi Adam,

In situations where you have impredicative set and aren't defining a
universe Venanzio Caprettas method works,
http://www.cs.ru.nl/~venanzio/publications/induction_recursion.pdf


> I could have something like:
> Inductive data_prop ...
> ...
> ...
> with Fixpoint func (data_prop).

Hi Dimitry, what would this look like without the '...'s?

-- 
View this message in context: 
http://www.nabble.com/Data-Structures-tp22535211p22562792.html
Sent from the Coq mailing list archive at Nabble.com.