The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

"Informative" and "logical" are fine. The word "Prop-bounded" is just weird in my opinion. Informally, people usually say "in Type" and "in Prop". Sometimes "proof-relevant" and "proof-irrelevant" are used (even though Prop does not actually have the proof irrelevance property, differences between proofs cannot be observed). I have also used "dynamic" and "static" (which, at the end of the day, are just another way to say "informative" and "logical", I guess).

On 30 September 2015 at 10:03, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

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,
>