From ec558e4f6bfad5bcbe2a85bf473a2563e193d669 Mon Sep 17 00:00:00 2001 From: MathisBD Date: Mon, 30 Dec 2024 16:38:38 +0100 Subject: [PATCH] update documentation --- common/theories/Environment.v | 37 +++++++++++++++++++---------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/common/theories/Environment.v b/common/theories/Environment.v index b5c0a3298..b7c5005fe 100644 --- a/common/theories/Environment.v +++ b/common/theories/Environment.v @@ -320,13 +320,15 @@ Module Environment (T : Term). (** Constructor name, without the module path. *) cstr_name : ident; (** Arguments of the constructor, which can depend on the inductives in the same block - and the parameters of the inductive. *) + and the parameters of the inductive : `ind_bodies ,,, ind_params |- cstr_args`. *) cstr_args : context; (** Indices of the constructor, which can depend on the inductives in the same block, - the parameters of the inductive and the constructor arguments. *) + the parameters of the inductive and the constructor arguments : + `ind_bodies ,,, ind_params ,,, cstr_args |- cstr_indices`. *) cstr_indices : list term; - (** Full type of the constructor, which can depend on the inductives in the same block. - This should be equal to `forall mind_params cstr_args, I mind_params cstr_indices` *) + (** Full type of the constructor, which can depend on the inductives in the same block : + `ind_bodies |- cstr_type`. This should be equal to + `forall ind_params cstr_args, I ind_params cstr_indices` *) cstr_type : term; (** Number of arguments of the constructor, _without_ let-in arguments and _without_ parameters. This should be equal to `context_assumptions cstr_args`. *) @@ -340,7 +342,7 @@ Module Environment (T : Term). (** Relevance of the projection. *) proj_relevance : relevance; (** Type of the projection, wich can depend on the parameters of the inductive - and on the object we are projecting from. *) + and on the object we are projecting from : `ind_params ,,, x |- proj_type`. *) proj_type : term; }. @@ -353,7 +355,7 @@ Module Environment (T : Term). cstr_type := f arities c.(cstr_type); cstr_arity := c.(cstr_arity) |}. - (** Here npars should be the [context_assumptions] of the parameters context. *) + (** Here npars should be the `context_assumptions` of the parameters context. *) Definition map_projection_body npars f c := {| proj_name := c.(proj_name); proj_relevance := c.(proj_relevance); @@ -364,20 +366,21 @@ Module Environment (T : Term). Record one_inductive_body := { (** Name of the inductive, without the module path. *) ind_name : ident; - (** Indices of the inductive type, which can depend on the parameters of the inductive. *) + (** Indices of the inductive, which can depend on the parameters : + `ind_params |- ind_indices`. *) ind_indices : context; (** Sort of the inductive. *) ind_sort : Sort.t; (** Full type of the inductive. This should be equal to - `forall mind_params ind_indices, tSort ind_sort` *) + `forall ind_params ind_indices, tSort ind_sort` *) ind_type : term; - (** Allowed eliminations for this inductive. *) + (** Allowed eliminations for the inductive. *) ind_kelim : allowed_eliminations; - (** Constructors of this inductive. Order is important. *) + (** Constructors of the inductive. Order is important. *) ind_ctors : list constructor_body; (** Names and types of primitive projections, if any. *) ind_projs : list projection_body; - (** Relevance of the inductive definition. *) + (** Relevance of the inductive. *) ind_relevance : relevance }. Definition map_one_inductive_body npars arities f m := @@ -392,7 +395,7 @@ Module Environment (T : Term). (** Data associated to a block of mutually inductive types. *) Record mutual_inductive_body := { - (** Whether the mutual inductive is inductive, coinductive or non-recursive. *) + (** Whether the block is inductive, coinductive or non-recursive (Records). *) ind_finite : recursivity_kind; (** Number of parameters (including non-uniform ones), _without_ counting let-in parameters. This should be equal to `context_assumptions ind_params`. *) @@ -404,19 +407,19 @@ Module Environment (T : Term). (** Whether the mutual inductive is universe monomorphic or universe polymorphic, and information about the local universes if polymorphic. *) ind_universes : universes_decl; - (** Variance information. [None] when non-cumulative. *) + (** Variance information. `None` when non-cumulative. *) ind_variance : option (list Universes.Variance.t) }. - (** Data associated to a constant (definition, lemma, axiom). *) + (** Data associated to a constant (definition, lemma or axiom). *) Record constant_body := { - (** Type of this constant. *) + (** Type of the constant. *) cst_type : term; - (** Body of this constant. For axioms this is [None]. *) + (** Body of the constant. For axioms this is [None]. *) cst_body : option term; (** Whether the constant is universe monomorphic or polymorphic, and if polymorphic information about its local universes. *) cst_universes : universes_decl; - (** Relevance of this constant. *) + (** Proof relevance of this constant. *) cst_relevance : relevance }. Definition map_constant_body f decl :=