The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello. Isn't possible to prove and use an appropriate induction 
principle for { T | term_is_correct T} with correct bindings inside of them?

Le 16/02/2016 18:38, Ilmārs Cīrulis a écrit :
> // Somehow I wrote answer but it got lost and wasn't send.
> Thank you, but this isn't good enough. If my idea isn't possible, then 
> I will simply write inductive definition of Term, then Fixpoint on it 
> (smth like term_is_correct) and use it inside type { T | 
> term_is_correct T}.
> But it would be unsatisfying for me. Because I need only correct Term 
> instances (with correct bindings inside of them) and have no use for 
> incorrect ones. :|
>
> If such mutual definition - of an inductive type which uses (in 
> definition) a fixpoint defined on it - isn't possible in Coq, I will, 
> of course, accept it and use sigma type.