Module AllScheme

Strictly Positive Uniform Parameters
val compute_params_rec_strpos : Environ.env -> Names.MutInd.t -> Declarations.mutual_inductive_body -> bool list

Computes which uniform parameters are strictly positive in a mutual inductive body

Lookup All Predicate and its Theorem
val compute_positive_uparams_and_suffix : Environ.env -> Names.MutInd.t -> Declarations.mutual_inductive_body -> Names.Id.t list option -> bool list * (string * string) * (string * string)

Compute the default positivity of the uniform parameters, and generates the suffix for naming the all predicate, and its predicate, as well as the key for registering. If a positivity specification is given by users bool list option, it is checked to be included in the default one, and the suffix are modified accordingly.

module Warning_scheme_all : sig ... end
val lookup_all_theorem : Names.inductive -> Names.GlobRef.t -> bool list -> (bool * Names.GlobRef.t * Names.GlobRef.t, Warning_scheme_all.t) Stdlib.result

Lookup the partial all predicate and its theorem for ind_nested for args_are_nested. If they are not found, lookup the general all predicate and its theorem. Returns if the partial all was found, and the global references. Return ind_nested if none is found.

Instantiate the All Predicate and its Theorem
val make_all_predicate : partial_nesting:bool -> Names.GlobRef.t -> bool list -> EConstr.constr array -> EConstr.constr option array -> EConstr.constr array -> EConstr.constr -> EConstr.constr LibBinding.State.t

Make the all predicate for a fresh instance and using Typing.checked_appvect, given:

  • whether the all predicate is the partial one, or the general one partial_nesting:bool
  • the positivity of each uniform parameter bool list
  • the instantiation of the uniform parameter of the inductive type constr array
  • the instation of the fresh predicate constr option array, using fun ... => True if the values are none, and all is the general predicate
  • the instantiation of the non-uniform parameters and indices
  • the argument to apply it to
val make_all_theorem : partial_nesting:bool -> Names.GlobRef.t -> bool list -> EConstr.constr array -> EConstr.constr option array -> EConstr.constr option array -> EConstr.constr array -> EConstr.constr -> EConstr.constr LibBinding.State.t

Make the theorem for the all predicate for a fresh instance and using Typing.checked_appvect, given:

  • whether the all predicate is the partial one, or the general one partial_nesting:bool
  • the positivity of each uniform parameter bool list
  • the instantiation of the uniform parameter of the inductive type constr array
  • the instation of the fresh predicate and the proofs they hold constr option array, using fun ... => True and fun _ => I if the values are none, and all is the general predicate
  • the instantiation of the non-uniform parameters and indices
  • the argument to apply it to
View for Arguments
type head_argument =
  1. | ArgIsSPUparam of int * EConstr.constr array
    (*

    position of the uniform parameter, args

    *)
  2. | ArgIsInd of int * EConstr.constr array * EConstr.constr array
    (*

    position of the one_inductive body, inst_nuparams, inst_indices

    *)
  3. | ArgIsNested of Names.GlobRef.t * bool list * EConstr.rel_context * EConstr.constr array * EConstr.constr array
    (*

    nested_container, strict positivity of its uniform parameters, uniform parameters, their instantiation, and instantiation of both non_uniform parameters and indices

    *)
  4. | ArgIsCst

View to decompose arguments as forall locs, X where X is further decomposed as a uniform parameter, the inductive, a nested argument or a constant.

Decompose the argument in it_Prod_or_LetIn local, X where X is a uniform parameter, Ind, nested or a constant

Generate All Predicate
Generate the Theorem for the All Predicate