Module `Kernel.Unchecked`Source

Sourcetype sub_ps_bp = {

sub_ps : Unchecked_types.Unchecked_types(Coh).sub_ps;
l : Unchecked_types.Unchecked_types(Coh).tm;
r : Unchecked_types.Unchecked_types(Coh).tm;

}

Sourceval ps_to_string : Common.ps -> string

Sourceval ty_to_string : Unchecked_types.Unchecked_types(Coh).ty -> string

Sourceval tm_to_string : Unchecked_types.Unchecked_types(Coh).tm -> string

val sub_ps_to_string : 
  ?func:(Common.Var.t * int) list list ->
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  string

Sourceval ctx_to_string : Unchecked_types.Unchecked_types(Coh).ctx -> string

Sourceval sub_to_string : Unchecked_types.Unchecked_types(Coh).sub -> string

Source

val meta_ctx_to_string : 
  Unchecked_types.Unchecked_types(Coh).meta_ctx ->
  string

Sourceval coh_pp_data_to_string : ?print_func:bool -> Common.coh_pp_data -> string

Sourceval full_name : Common.coh_pp_data -> string

Source

val check_equal_ctx : 
  Unchecked_types.Unchecked_types(Coh).ctx ->
  Unchecked_types.Unchecked_types(Coh).ctx ->
  unit

Sourceval check_equal_ps : Common.ps -> Common.ps -> unit

Source

val check_equal_ty : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  Unchecked_types.Unchecked_types(Coh).ty ->
  unit

Source

val check_equal_tm : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Unchecked_types.Unchecked_types(Coh).tm ->
  unit

Sourceval dim_ctx : Unchecked_types.Unchecked_types(Coh).ctx -> int

Sourceval dim_ty : Unchecked_types.Unchecked_types(Coh).ty -> int

Sourceval dim_ps : Common.ps -> int

Sourceval ps_to_ctx : Common.ps -> Unchecked_types.Unchecked_types(Coh).ctx

Sourceval identity_ps : Common.ps -> Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val tm_apply_sub : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Unchecked_types.Unchecked_types(Coh).sub ->
  Unchecked_types.Unchecked_types(Coh).tm

Source

val ty_apply_sub : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  Unchecked_types.Unchecked_types(Coh).sub ->
  Unchecked_types.Unchecked_types(Coh).ty

Source

val sub_ps_apply_sub : 
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).sub ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val ty_apply_sub_ps : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).ty

Source

val tm_apply_sub_ps : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).tm

Source

val sub_ps_apply_sub_ps : 
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val ty_sub_preimage : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  Unchecked_types.Unchecked_types(Coh).sub ->
  Unchecked_types.Unchecked_types(Coh).ty

Source

val db_levels : 
  Unchecked_types.Unchecked_types(Coh).ctx ->
  Unchecked_types.Unchecked_types(Coh).ctx * (Common.Var.t * int) list * int

Source

val db_level_sub : 
  Unchecked_types.Unchecked_types(Coh).ctx ->
  Unchecked_types.Unchecked_types(Coh).sub

Source

val db_level_sub_inv : 
  Unchecked_types.Unchecked_types(Coh).ctx ->
  Unchecked_types.Unchecked_types(Coh).sub

Source

val rename_ty : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  (Common.Var.t * int) list ->
  Unchecked_types.Unchecked_types(Coh).ty

Source

val rename_tm : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  (Common.Var.t * int) list ->
  Unchecked_types.Unchecked_types(Coh).tm

Source

val tm_contains_var : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Common.Var.t ->
  bool

Source

val ty_contains_var : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  Common.Var.t ->
  bool

Source

val tm_contains_vars : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Common.Var.t list ->
  bool

Source

val sub_ps_to_sub : 
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).sub

Source

val sub_to_sub_ps : 
  Common.ps ->
  Unchecked_types.Unchecked_types(Coh).sub ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Sourceval suspend_ps : Common.ps -> Common.ps

Source

val suspend_ty : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  Unchecked_types.Unchecked_types(Coh).ty

Source

val suspend_tm : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Unchecked_types.Unchecked_types(Coh).tm

Source

val suspend_ctx : 
  Unchecked_types.Unchecked_types(Coh).ctx ->
  Unchecked_types.Unchecked_types(Coh).ctx

Source

val suspend_sub_ps : 
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Sourceval ps_bdry : Common.ps -> Common.ps

Sourceval ps_src : Common.ps -> Unchecked_types.Unchecked_types(Coh).sub_ps

Sourceval ps_tgt : Common.ps -> Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val tm_sub_preimage : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Unchecked_types.Unchecked_types(Coh).sub ->
  Unchecked_types.Unchecked_types(Coh).tm

Source

val suspwedge_subs_ps : 
  Unchecked_types.Unchecked_types(Coh).sub_ps list ->
  Common.ps list ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val opsuspwedge_subs_ps : 
  Unchecked_types.Unchecked_types(Coh).sub_ps list ->
  Common.ps list ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val canonical_inclusions : 
  Common.ps list ->
  Unchecked_types.Unchecked_types(Coh).sub_ps list

Source

val ps_compose : 
  int ->
  Common.ps ->
  Common.ps ->
  Common.ps
  * Unchecked_types.Unchecked_types(Coh).sub_ps
  * Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val pullback_up : 
  int ->
  Common.ps ->
  Common.ps ->
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val ty_to_sub_ps : 
  Unchecked_types.Unchecked_types(Coh).ty ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val coh_to_sub_ps : 
  Unchecked_types.Unchecked_types(Coh).tm ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val sub_ps_to_sub_ps_bp : 
  Unchecked_types.Unchecked_types(Coh).sub_ps ->
  sub_ps_bp

Source

val wedge_sub_ps_bp : 
  sub_ps_bp list ->
  Unchecked_types.Unchecked_types(Coh).sub_ps

Source

val list_to_sub : 
  Unchecked_types.Unchecked_types(Coh).tm list ->
  Unchecked_types.Unchecked_types(Coh).ctx ->
  Unchecked_types.Unchecked_types(Coh).sub

Source

val list_to_db_level_sub : 
  Unchecked_types.Unchecked_types(Coh).tm list ->
  Unchecked_types.Unchecked_types(Coh).sub

package catt

Module Kernel.UncheckedSource

Module `Kernel.Unchecked`Source