package catt

You can search for identifiers within the package.

in-package search v0.2.0

catt
- Library catt
  - Catt
    
    Builtin
    
    Command
    
    Common
    
    Var
    
    Cubical_composite
    
    Elaborate
    
    Environment
    
    Error
    
    Functorialisation
    
    Inverse
    
    Io
    
    Kernel
    
    Coh
    
    Ctx
    
    Ty
    
    Tm
    
    PS
    
    Unchecked
    
    Lexer
    
    Meta
    
    Opposite
    
    Parser
    
    Prover
    
    Ps_reduction
    
    Raw
    
    Raw_types
    
    Settings
    
    Std
    
    List
    
    Suspension
    
    Telescope
    
    Translate_raw
    
    Unchecked
    
    Unchecked
    
    Make
    
    Unchecked_types
    
    Unchecked_types_sig
    
    Unchecked_types
- Sources
  - catt
    
    builtin.ml
    
    catt.ml
    
    command.ml
    
    common.ml
    
    cubical_composite.ml
    
    elaborate.ml
    
    environment.ml
    
    error.ml
    
    functorialisation.ml
    
    inverse.ml
    
    io.ml
    
    kernel.ml
    
    lexer.ml
    
    meta.ml
    
    opposite.ml
    
    parser.ml
    
    prover.ml
    
    ps_reduction.ml
    
    raw.ml
    
    settings.ml
    
    std.ml
    
    suspension.ml
    
    telescope.ml
    
    translate_raw.ml
    
    unchecked.ml
    
    unchecked_types.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Catt.Kernel`Source

Sourcemodule Coh : sig ... end

Sourcemodule Ctx : sig ... end

Sourcemodule Ty : sig ... end

Sourcemodule Tm : sig ... end

Sourcemodule PS : sig ... end

Sourcemodule Unchecked : sig ... end

val check_term : 
  Ctx.t ->
  ?ty:Unchecked_types.Unchecked_types(Coh).ty ->
  Unchecked_types.Unchecked_types(Coh).tm ->
  Tm.t

val check_coh : 
  Common.ps ->
  Unchecked_types.Unchecked_types(Coh).ty ->
  Common.coh_pp_data ->
  Coh.t