package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/extraction_plugin/Extraction_plugin/Mlutil/index.html

Module Extraction_plugin.MlutilSource

Sourceval reset_meta_count : unit -> unit
Sourceval new_meta : 'a -> Miniml.ml_type
Sourceval type_subst_list : Miniml.ml_type list -> Miniml.ml_type -> Miniml.ml_type
Sourceval type_subst_vect : Miniml.ml_type array -> Miniml.ml_type -> Miniml.ml_type
Sourceval instantiation : Miniml.ml_schema -> Miniml.ml_type
Sourceval needs_magic : (Miniml.ml_type * Miniml.ml_type) -> bool
Sourceval put_magic_if : bool -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval generalizable : Miniml.ml_ast -> bool
Sourcemodule Mlenv : sig ... end
Sourceval type_mem_kn : Names.MutInd.t -> Miniml.ml_type -> bool
Sourceval type_maxvar : Miniml.ml_type -> int
Sourceval type_recomp : (Miniml.ml_type list * Miniml.ml_type) -> Miniml.ml_type
Sourcetype abbrev_map = Miniml.global -> Miniml.ml_type option
Sourceval type_to_signature : abbrev_map -> Miniml.ml_type -> Miniml.signature
Sourceval type_expunge_from_sign : abbrev_map -> Miniml.signature -> Miniml.ml_type -> Miniml.ml_type
Sourceval eq_ml_type : Miniml.ml_type -> Miniml.ml_type -> bool
Sourceval isTdummy : Miniml.ml_type -> bool
Sourceval isMLdummy : Miniml.ml_ast -> bool
Sourceval isKill : Miniml.sign -> bool
Sourceval anonymous_name : Names.Id.t
Sourceval dummy_name : Names.Id.t
Sourceval id_of_name : Names.Name.t -> Names.Id.t
Sourceval id_of_mlid : Miniml.ml_ident -> Names.Id.t
Sourceval collect_n_lams : int -> Miniml.ml_ast -> Miniml.ml_ident list * Miniml.ml_ast
Sourceval remove_n_lams : int -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval nb_lams : Miniml.ml_ast -> int
Sourceval dummy_lams : Miniml.ml_ast -> int -> Miniml.ml_ast
Sourceval anonym_or_dummy_lams : Miniml.ml_ast -> Miniml.signature -> Miniml.ml_ast
Sourceval eta_args_sign : int -> Miniml.signature -> Miniml.ml_ast list
Sourceval ast_map_lift : (int -> Miniml.ml_ast -> Miniml.ml_ast) -> int -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval ast_iter : (Miniml.ml_ast -> unit) -> Miniml.ml_ast -> unit
Sourceval ast_occurs : int -> Miniml.ml_ast -> bool
Sourceval ast_occurs_itvl : int -> int -> Miniml.ml_ast -> bool
Sourceval ast_lift : int -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval dump_unused_vars : Miniml.ml_ast -> Miniml.ml_ast
Sourceval optimize_fix : Miniml.ml_ast -> Miniml.ml_ast
Sourceval inline : Table.t -> Miniml.global -> Miniml.ml_ast -> bool
Sourceval is_basic_pattern : Miniml.ml_pattern -> bool
Sourceval has_deep_pattern : Miniml.ml_branch array -> bool
Sourceval is_regular_match : Miniml.ml_branch array -> bool
Sourceexception Impossible
Sourcetype sign_kind =
  1. | EmptySig
  2. | NonLogicalSig
  3. | SafeLogicalSig
  4. | UnsafeLogicalSig
Sourceval sign_no_final_keeps : Miniml.signature -> Miniml.signature