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/ltac2_plugin/Ltac2_plugin/Tac2typing_env/index.html

Module Ltac2_plugin.Tac2typing_envSource

Sourcemodule TVar : sig ... end
Sourcetype t
Sourceval empty_env : ?strict:bool -> unit -> t

default strict:true

Sourceval set_rec : (Names.KerName.t * int) Names.Id.Map.t -> t -> t
Sourceval reject_unbound_tvar : t -> t
Sourceval env_strict : t -> bool
Sourceval env_name : t -> TVar.t -> string
Sourceval fresh_id : t -> TVar.t
Sourceval get_alias : Names.lident -> t -> TVar.t
Sourceval find_rec_var : Names.Id.t -> t -> (Names.KerName.t * int) option
Sourcetype mix_var =
  1. | GVar of TVar.t
  2. | LVar of int
Sourcetype mix_type_scheme = int * mix_var Tac2expr.glb_typexpr
Sourceval mem_var : Names.Id.t -> t -> bool
Sourceval find_var : Names.Id.t -> t -> mix_type_scheme
Sourceval is_used_var : Names.Id.t -> t -> bool
Sourceval bound_vars : t -> Names.Id.Set.t

View function, allows to ensure head normal forms

Sourceval pr_glbtype : t -> TVar.t Tac2expr.glb_typexpr -> Pp.t
Sourceval eq_or_tuple : ('a -> 'b -> bool) -> 'a Tac2expr.or_tuple -> 'b Tac2expr.or_tuple -> bool

unify0 raises CannotUnify, unify raises usererror

Sourceval push_name : Names.Name.t -> mix_type_scheme -> t -> t
Sourceval normalize : t -> (int Stdlib.ref * int Tac2expr.glb_typexpr TVar.Map.t Stdlib.ref) -> TVar.t Tac2expr.glb_typexpr -> int Tac2expr.glb_typexpr