package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
module TVar : sig ... end
type t
val empty_env : ?strict:bool -> unit -> t

default strict:true

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

View function, allows to ensure head normal forms

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

unify0 raises CannotUnify, unify raises usererror

val unify : ?loc:Loc.t -> t -> TVar.t Tac2expr.glb_typexpr -> TVar.t Tac2expr.glb_typexpr -> unit
val abstract_var : t -> TVar.t Tac2expr.glb_typexpr -> mix_type_scheme
val push_name : Names.Name.t -> mix_type_scheme -> t -> t
val push_ids : mix_type_scheme Names.Id.Map.t -> t -> t
val subst_type : ('a -> 'b Tac2expr.glb_typexpr) -> 'a Tac2expr.glb_typexpr -> 'b Tac2expr.glb_typexpr
val 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