Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Question of terminology

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question of terminology


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Question of terminology
  • Date: Tue, 29 Sep 2015 11:13:23 +0200
  • Organization: LORIA

Dear all,

I wonder if there exists a term to characterise the difference between
definitions over the Type sort for definitions over the Prop sort.

For instance, let us consider the following:

(********************)

Require Import List.

Set Implicit Arguments.

Definition repr X (P : X -> Prop) l := forall x, In x l <-> P x.

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.

(*******************)

Should I speak about the "Prop-bounded" or "Type-bounded" version of
the "finite" inductive predicate (this is a word that I encountered
in Coq source Coq somewhere) ? Or is there a better way to denote the
difference between those two (nearly isomorphic) definitions.

Of course, I know why there is a difference and that finite_t is
stronger (in Type context) that finite but my question is more
about the terminology.

Thanks in advance for any hints.

Dominique



Archive powered by MHonArc 2.6.18.

Top of Page