The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

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,

-- 
Stéphane