The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Thank you Stéphane,

Indeed "informative" vs "logical" seems to be a good way to
distinguish "finite_t" from "finite". But may be it is a bit too
much related to extraction.

What about the term "Prop-bounded" which is used for example
in the title of

"A Coinductive Monad for Prop-Bounded Recursion" by A. Megacz

Do you think "Prop-bounded" or "Type-bounded" covers the
distinction I am trying to make ?

Cheers,

Dominique

---------------------


On 09/29/2015 05:41 PM, Stéphane Glondu wrote:
> Le 29/09/2015 11:13, Dominique Larchey-Wendling a écrit :
>> I wonder if there exists a term to characterise the difference between
>> definitions over the Type sort for definitions over the Prop sort.
>> [...]
>> Inductive finite X (P : X -> Prop) : Prop :=
>>   | in_finite : forall l, repr P l -> finite P.
>>
>> Inductive finite_t X (P : X -> Prop) : Type :=
>>   | in_finite_t : forall l, repr P l -> finite_t P.
> 
> In the extraction context, finite is said "logical" and finite_t
> "informative". See [1].
> 
> [1] https://hal.archives-ouvertes.fr/hal-00150914/document
> 
> Cheers,
>