package rocq-runtime

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

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
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