package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TermopsSource

This file defines various utilities for term manipulation that are not needed in the kernel.

about contexts

Sourceval push_named_rec_types : (Names.Name.t Constr.binder_annot array * Constr.types array * 'a) -> Environ.env -> Environ.env
Sourceval lookup_rel_id : Names.Id.t -> ('c, 't, 'r) Context.Rel.pt -> int * 'c option * 't

Associates the contents of an identifier in a rel_context. Raise Not_found if there is no such identifier.

Sourceval rel_vect : int -> int -> Constr.constr array

Functions that build argument lists matching a block of binders or a context. rel_vect n m builds |Rel (n+m);...;Rel(n+1)|

Sourceval rel_list : int -> int -> EConstr.constr list

Prod/Lambda/LetIn destructors on econstr

  • deprecated Use synonymous [EConstr.mkProd_or_LetIn].
  • deprecated Use synonymous [EConstr.mkProd_wo_LetIn].
  • deprecated Use synonymous [EConstr.it_mkProd].
  • deprecated Use synonymous [EConstr.it_mkLambda].
  • deprecated Use synonymous [EConstr.it_mkProd_or_LetIn].
  • deprecated Use synonymous [EConstr.it_mkProd_wo_LetIn].
Sourceval it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
  • deprecated Use synonymous [Term.it_mkLambda_or_LetIn].
  • deprecated Use synonymous [EConstr.it_mkNamedProd_or_LetIn].
  • deprecated Use synonymous [EConstr.it_mkNamedLambda_or_LetIn].

Prod/Lambda/LetIn destructors on constr

Sourceval it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
Sourceval it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
Generic iterators on constr
Sourceval map_constr_with_binders_left_to_right : Environ.env -> Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
Sourceval map_constr_with_full_binders : Environ.env -> Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
Sourceval fold_constr_with_full_binders : Environ.env -> Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
Sourceval drop_extra_implicit_args : Evd.evar_map -> EConstr.constr -> EConstr.constr

occur checks

Sourceexception Occur
Sourceval occur_meta : Evd.evar_map -> EConstr.constr -> bool
Sourceval occur_existential : Evd.evar_map -> EConstr.constr -> bool
Sourceval occur_meta_or_existential : Evd.evar_map -> EConstr.constr -> bool
Sourceval occur_metavariable : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
Sourceval occur_evar : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
Sourceval occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
Sourceval occur_var_indirectly : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> Names.GlobRef.t option
Sourceval occur_var_in_decl : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.named_declaration -> bool
Sourceval local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool

As occur_var but assume the identifier not to be a section variable

Sourceval local_occur_var_in_decl : Evd.evar_map -> Names.Id.t -> EConstr.named_declaration -> bool
Sourceval free_rels_and_unqualified_refs : Evd.evar_map -> EConstr.constr -> Int.Set.t * Names.Id.Set.t
Sourceval dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool

dependent m t tests whether m is a subterm of t

Sourceval dependent_no_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
Sourceval dependent_in_decl : Evd.evar_map -> EConstr.constr -> EConstr.named_declaration -> bool
Sourceval count_occurrences : Evd.evar_map -> EConstr.constr -> EConstr.constr -> int
Sourceval collect_metas : Evd.evar_map -> EConstr.constr -> int list

for visible vars only

Sourcetype meta_value_map = (Constr.metavariable * Constr.constr) list
Sourcetype meta_type_map = (Constr.metavariable * Constr.types) list

Type assignment for metavariables

pop c lifts by -1 the positive indexes in c

...

Substitution of an arbitrary large term. Uses equality modulo reduction of let

Sourceval replace_term_gen : Evd.evar_map -> (Evd.evar_map -> int -> EConstr.constr -> bool) -> int -> EConstr.constr -> EConstr.constr -> EConstr.constr

replace_term_gen eq arity e c replaces matching subterms according to eq by e in c. If arity is non-zero applications of larger length are handled atomically.

subst_term d c replaces d by Rel 1 in c

replace_term d e c replaces d by e in c

Sourceval base_sort_cmp : Conversion.conv_pb -> Sorts.t -> Sorts.t -> bool

Alternative term equalities

prod_applist forall (x1:B1;...;xn:Bn), B a1...an

  • returns

    B[a1...an]

Sourceval prod_applist_decls : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr

In prod_applist_decls n c args, c is supposed to have the form ∀Γ.c with Γ of length m and possibly with let-ins; it returns c with the assumptions of Γ instantiated by args and the local definitions of Γ expanded. Note that n counts both let-ins and prods, while the length of args only counts prods. In other words, varying n changes how many trailing let-ins are expanded.

Sourceval strip_outer_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr

Remove recursively the casts around a term i.e. strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c.

Sourceval nb_lam : Evd.evar_map -> EConstr.constr -> int

nb_lam $ x_1:T_1...x_n:T_nc $ where $ c $ is not an abstraction gives $ n $ (casts are ignored)

Sourceval nb_prod : Evd.evar_map -> EConstr.constr -> int

Similar to nb_lam, but gives the number of products instead

Sourceval nb_prod_modulo_zeta : Evd.evar_map -> EConstr.constr -> int

Similar to nb_prod, but zeta-contracts let-in on the way

Get the last arg of a constr intended to be an application

Sourcetype names_context = Names.Name.t list

name contexts

Sourceval lookup_name_of_rel : int -> names_context -> Names.Name.t
Sourceval lookup_rel_of_name : Names.Id.t -> names_context -> int
Sourceval empty_names_context : names_context
Sourceval ids_of_rel_context : ('c, 't, 'r) Context.Rel.pt -> Names.Id.t list
Sourceval ids_of_named_context : ('c, 't, 'r) Context.Named.pt -> Names.Id.t list
Sourceval ids_of_context : Environ.env -> Names.Id.t list
Sourceval names_of_rel_context : Environ.env -> names_context
  • deprecated Use synonymous [Context.Rel.chop_nhyps].
Sourceval env_rel_context_chop : int -> Environ.env -> Environ.env * EConstr.rel_context
Sourceval vars_of_env : Environ.env -> Names.Id.Set.t

Set of local names

other signature iterators

Sourceval assums_of_rel_context : ('c, 't, 'r) Context.Rel.pt -> ((Names.Name.t, 'r) Context.pbinder_annot * 't) list
Sourceval lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.lift_rel_context].
Sourceval substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.substl_rel_context].
Sourceval smash_rel_context : Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.smash_rel_context].
Sourceval map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c, 'r) Context.Rel.pt -> ('c, 'c, 'r) Context.Rel.pt
  • deprecated Use synonymous [Context.Rel.map_with_binders].
Sourceval fold_named_context_both_sides : ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> Constr.named_context -> init:'a -> 'a
Sourceval mem_named_context_val : Names.Id.t -> Environ.named_context_val -> bool
Sourceval map_rel_decl : ('r1 -> 'r2) -> ('a -> 'b) -> ('a, 'a, 'r1) Context.Rel.Declaration.pt -> ('b, 'b, 'r2) Context.Rel.Declaration.pt
  • deprecated Use [Context.Rel.Declaration.map_constr_het]
Sourceval map_named_decl : ('r1 -> 'r2) -> ('a -> 'b) -> ('a, 'a, 'r1) Context.Named.Declaration.pt -> ('b, 'b, 'r2) Context.Named.Declaration.pt
  • deprecated Use [Context.Named.Declaration.map_constr_het]
Sourceval clear_named_body : Names.Id.t -> Environ.env -> Environ.env

Gives an ordered list of hypotheses, closed by dependencies, containing a given set

Sourceval is_section_variable : Environ.env -> Names.Id.t -> bool

Test if an identifier is the basename of a global reference

  • deprecated Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
  • deprecated Use [EConstr.isRefX] instead.
Sourceval isGlobalRef : Evd.evar_map -> EConstr.constr -> bool
  • deprecated Use [EConstr.isRef] instead.
Sourceval is_template_polymorphic_ind : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
Sourceval is_Prop : Evd.evar_map -> EConstr.constr -> bool
Sourceval is_Set : Evd.evar_map -> EConstr.constr -> bool
Sourceval is_Type : Evd.evar_map -> EConstr.constr -> bool
Sourceval reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
Debug pretty-printers
Sourceval pr_global_env : Environ.env -> Names.GlobRef.t -> Pp.t
Sourceval pr_existential_key : Environ.env -> Evd.evar_map -> Evar.t -> Pp.t
Sourceval evar_suggested_name : Environ.env -> Evd.evar_map -> Evar.t -> Names.Id.t
Sourceval pr_evar_info : Environ.env -> Evd.evar_map -> 'a Evd.evar_info -> Pp.t
Sourceval pr_evar_constraints : Evd.evar_map -> Evd.evar_constraint list -> Pp.t
Sourceval pr_evar_map : ?with_univs:bool -> int option -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> Evd.any_evar_info -> bool) -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_metaset : Evd.Metaset.t -> Pp.t
Sourceval pr_evar_universe_context : UState.t -> Pp.t
Sourceval pr_evd_level : Evd.evar_map -> Univ.Level.t -> Pp.t
Sourceval pr_evd_qvar : Evd.evar_map -> Sorts.QVar.t -> Pp.t
Sourcemodule Internal : sig ... end

NOTE: to print terms you always want to use functions in Printer, not these ones which are for very special cases.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct