coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Question of terminology, Dominique Larchey-Wendling, 09/29/2015
- Re: [Coq-Club] Question of terminology, Stéphane Glondu, 09/29/2015
- Re: [Coq-Club] Question of terminology, Dominique Larchey-Wendling, 09/30/2015
- Re: [Coq-Club] Question of terminology, Arnaud Spiwack, 09/30/2015
- Re: [Coq-Club] Question of terminology, Dominique Larchey-Wendling, 09/30/2015
- Re: [Coq-Club] Question of terminology, Stéphane Glondu, 09/29/2015
Archive powered by MHonArc 2.6.18.