| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/pretyping/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 5 kB |
|
Quelle glob_ops.mli Sprache: SML |
|||||||||
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Glob_term val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen val glob_Type_sort : glob_sort val glob_SProp_sort : glob_sort val glob_Prop_sort : glob_sort val glob_Set_sort : glob_sort (** Equalities *) val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool val glob_qvar_eq : glob_qvar -> glob_qvar -> bool val glob_quality_eq : glob_quality -> glob_quality -> bool val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool val relevance_info_eq : relevance_info -> relevance_info -> bool val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool (** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if contains a max, an increment, or a flexible universe *) exception ComplexSort val glob_sort_quality : glob_sort -> UnivGen.QualityOrSet.t val fresh_glob_sort_in_quality : Evd.evar_map -> glob_sort -> Evd.evar_map * Evd.esorts val alias_of_pat : 'a cases_pattern_g -> Name.t val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g val cast_kind_eq : Constr.cast_kind -> Constr.cast_kind -> bool val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool (** Operations on [glob_constr] *) val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list (** Apply a list of arguments to a glob_constr *) val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g list -> 'a glob_constr_g val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr (** Equality on [binding_kind] *) val binding_kind_eq : binding_kind -> binding_kind -> bool (** Ensure traversal from left to right *) val map_glob_constr_left_to_right : (glob_constr -> glob_constr) -> glob_constr -> glob_constr val map_glob_constr_left_to_right_with_names : (glob_constr -> glob_constr) -> (Name.t -> Name.t) -> glob_constr -> glob_constr val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) -> (Name.t -> Name.t -> glob_constr option -> glob_constr option -> bool) -> glob_constr -> glob_constr -> bool val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool val free_glob_vars : 'a glob_constr_g -> Id.Set.t val bound_glob_vars : glob_constr -> Id.Set.t (* Obsolete *) val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option val glob_visible_short_qualid : 'a glob_constr_g -> Id.Set.t (* Renaming free variables using a renaming map; fails with [UnsoundRenaming] if applying the renaming would introduce collision, as in, e.g., renaming [P x y] using substitution [(x,y)]; inner alpha-conversion done only for forall, fun, let but not for cases and fix *) exception UnsoundRenaming val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_g (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented here by its relevant components [m] and [c]. It is used to interpret Ltac-bound names both in pretyping and printing of terms. *) val map_pattern_binders : (Name.t -> Name.t) -> tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses) (** [map_pattern f m c] applies [f] to the return predicate and the right-hand side of a pattern-matching expression ({!Glob_term.GCases}) represented here by its relevant components [m] and [c]. *) val map_pattern : (glob_constr -> glob_constr) -> tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses) (** Conversion from glob_constr to cases pattern, if possible Evaluation is forced. Take the current alias as parameter, @raise Not_found if translation is impossible *) val cases_pattern_of_glob_constr : Environ.env -> Name.t -> 'a glob_constr_g -> 'a cases_p val glob_constr_of_closed_cases_pattern : Environ.env -> 'a cases_pattern_g -> Name.t (** A canonical encoding of cases pattern into constr such that composed with [cases_pattern_of_glob_constr Anonymous] gives identity *) val glob_constr_of_cases_pattern : Environ.env -> 'a cases_pattern_g -> 'a glob_constr_ val add_patterns_for_params_remove_local_defs : Environ.env -> constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list val empty_lvar : Ltac_pretype.ltac_var_map val kind_of_glob_kind : glob_evar_kind -> Evar_kinds.t val naming_of_glob_kind : glob_evar_kind -> Namegen.intro_pattern_naming_expr ¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28