catt 1.0 · OCaml Package

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

}

val ps_to_string : Common.ps -> string

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

val 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

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

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

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

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

val full_name : Common.coh_pp_data -> string

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

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

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

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

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

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

val dim_ps : Common.ps -> int

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val suspend_ps : Common.ps -> Common.ps

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

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

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

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

val ps_bdry : Common.ps -> Common.ps

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

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

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

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

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

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

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

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

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

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

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

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

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

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

package catt