Module `Ltac2_plugin.Tac2typing_env`Source

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 =

| GVar of TVar.t
| 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

Source

val get_variable0 : 
  (Names.Id.t -> bool) ->
  Tac2expr.tacref Tac2expr.or_relid ->
  Tac2expr.tacref Locus.or_var

Source

val get_variable : 
  t ->
  Tac2expr.tacref Tac2expr.or_relid ->
  Tac2expr.tacref Locus.or_var

Sourceval kind : t -> TVar.t Tac2expr.glb_typexpr -> TVar.t Tac2expr.glb_typexpr

View function, allows to ensure head normal forms

Sourceval pr_glbtype : t -> TVar.t Tac2expr.glb_typexpr -> Pp.t

Source

val eq_or_tuple : 
  ('a -> 'b -> bool) ->
  'a Tac2expr.or_tuple ->
  'b Tac2expr.or_tuple ->
  bool

Sourceexception CannotUnify of TVar.t Tac2expr.glb_typexpr * TVar.t Tac2expr.glb_typexpr

Source

val unify0 : 
  t ->
  TVar.t Tac2expr.glb_typexpr ->
  TVar.t Tac2expr.glb_typexpr ->
  unit

unify0 raises CannotUnify, unify raises usererror

Source

val unify : 
  ?loc:Loc.t ->
  t ->
  TVar.t Tac2expr.glb_typexpr ->
  TVar.t Tac2expr.glb_typexpr ->
  unit

Source

val unify_arrow : 
  ?loc:Loc.t ->
  t ->
  TVar.t Tac2expr.glb_typexpr ->
  (Loc.t option * TVar.t Tac2expr.glb_typexpr) list ->
  TVar.t Tac2expr.glb_typexpr

Sourceval abstract_var : t -> TVar.t Tac2expr.glb_typexpr -> mix_type_scheme

Sourceval monomorphic : TVar.t Tac2expr.glb_typexpr -> mix_type_scheme

Sourceval polymorphic : Tac2expr.type_scheme -> mix_type_scheme

Sourceval push_name : Names.Name.t -> mix_type_scheme -> t -> t

Sourceval push_ids : mix_type_scheme Names.Id.Map.t -> t -> t

Source

val subst_type : 
  ('a -> 'b Tac2expr.glb_typexpr) ->
  'a Tac2expr.glb_typexpr ->
  'b Tac2expr.glb_typexpr

Source

val normalize : 
  t ->
  (int Stdlib.ref * int Tac2expr.glb_typexpr TVar.Map.t Stdlib.ref) ->
  TVar.t Tac2expr.glb_typexpr ->
  int Tac2expr.glb_typexpr

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2typing_env/index.html

Module `Ltac2_plugin.Tac2typing_env`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2typing_env/index.html

Module Ltac2_plugin.Tac2typing_envSource

Module `Ltac2_plugin.Tac2typing_env`Source