catt 1.0 · OCaml Package

val coh_depth1 : 
  (Kernel.Coh.t ->
    Common.Var.t list ->
    Unchecked_types.Unchecked_types(Kernel.Coh).tm
    * Unchecked_types.Unchecked_types(Kernel.Coh).ctx)
    Stdlib.ref

val preimage : 
  Unchecked_types.Unchecked_types(Kernel.Coh).ctx ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps ->
  Common.Var.t list ->
  Common.Var.t list

val tgt_subst : 
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub

val coh : 
  Kernel.Coh.t ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm
  * Unchecked_types.Unchecked_types(Kernel.Coh).ctx

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

val coh_depth0 : Kernel.Coh.t -> Common.Var.t list -> Kernel.Coh.t

val coh_all : Kernel.Coh.t -> Kernel.Coh.t

val tm_one_step_tm : 
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm

val ty : 
  Unchecked_types.Unchecked_types(Kernel.Coh).ty ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ty

val ctx : 
  Unchecked_types.Unchecked_types(Kernel.Coh).ctx ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ctx

val sub_ps : 
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps

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

val ps : 
  Common.ps ->
  Common.Var.t list ->
  Common.ps * (Common.Var.t * int) list

val sub : 
  Unchecked_types.Unchecked_types(Kernel.Coh).sub ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub

val sub_w_tgt : 
  Common.ps ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps
  * Common.ps
  * (Common.Var.t * int) list
  * Common.Var.t list

val whisk_sub_ps : 
  int ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ty ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ty ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps

package catt