(************************************************************************) (* * 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) *) (************************************************************************)
(** Can raise [Not_found].
Beware that this is not exactly the reverse of [to_string] below. *) val parse : string -> t
val equal : t -> t -> bool
typeconst =
| Arraymaxlength
| Stringmaxlength
type arg_kind =
| Kparam (* not needed for the evaluation of the primitive*)
| Kwhnf (* need to be reduced in whnf before reducing the primitive *)
| Karg (* no need to be reduced in whnf *)
type args_red = arg_kind list
val hash : t -> int
val to_string : t -> string
val arity : t -> int (** Including parameters *)
val nparams : t -> int
val kind : t -> args_red (** Includes parameters *)
(** Special Entries for Register **)
type'a prim_type =
| PT_int63 : unit prim_type
| PT_float64 : unit prim_type
| PT_string : unit prim_type
| PT_array : (UVars.Instance.t * ind_or_type) prim_type
and'a prim_ind =
| PIT_bool : unit prim_ind
| PIT_carry : ind_or_type prim_ind
| PIT_pair : (ind_or_type * ind_or_type) prim_ind
| PIT_cmp : unit prim_ind
| PIT_f_cmp : unit prim_ind
| PIT_f_class : unit prim_ind
and ind_or_type =
| PITT_ind : 'a prim_ind * 'a -> ind_or_type
| PITT_type : 'a prim_type * 'a -> ind_or_type
| PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *)
val typ_univs : 'a prim_type -> UVars.AbstractContext.t
type prim_type_ex = PTE : 'a prim_type -> prim_type_ex
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
(** Can raise [Not_found] *) val prim_type_of_string : string -> prim_type_ex val prim_type_to_string : 'a prim_type -> string
type op_or_type =
| OT_op of t
| OT_type : 'a prim_type -> op_or_type
| OT_const ofconst
val op_or_type_univs : op_or_type -> UVars.AbstractContext.t
val prim_ind_to_string : 'a prim_ind -> string
(** Can raise [Not_found] *) val op_or_type_of_string : string -> op_or_type
val op_or_type_to_string : op_or_type -> string
val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
val univs : t -> UVars.AbstractContext.t
val types : t -> Constr.rel_context * ind_or_type list * ind_or_type (** Parameters * Reduction relevant arguments * output type
XXX we could reify universes in ind_or_type (currently polymorphic types
like array are assumed to use universe 0). *)
val body_of_prim_const : const -> Constr.t
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
