package catt

You can search for identifiers within the package.

in-package search v0.2.0

catt
- Catt
  - Builtin
  - Command
  - Common
    
    Var
  - Cubical_composite
  - Elaborate
  - Environment
  - Error
  - Functorialisation
  - Inverse
  - Io
  - Kernel
    
    Coh
    
    Ctx
    
    PS
    
    Tm
    
    Ty
    
    Unchecked
  - Lexer
  - Meta
  - Opposite
  - Parser
  - Prover
  - Ps_reduction
  - Raw
  - Raw_types
  - Settings
  - Std
    
    List
  - Suspension
  - Telescope
  - Translate_raw
  - Unchecked
    
    Unchecked
    
    Coh
    
    Make
    
    _
  - Unchecked_types
    
    Unchecked_types
    
    Coh
    
    Unchecked_types_sig
    
    Coh

Legend:
Library
Module
Module type
Parameter
Class
Class type

type cmd =

| Coh of Common.Var.t * (Common.Var.t * Raw_types.tyR) list * Raw_types.tyR
| Check of (Common.Var.t * Raw_types.tyR) list * Raw_types.tmR * Raw_types.tyR option
| Decl of Common.Var.t * (Common.Var.t * Raw_types.tyR) list * Raw_types.tmR * Raw_types.tyR option
| Set of string * string

type prog = cmd list

val postprocess_fn : 
  (Unchecked_types.Unchecked_types(Kernel.Coh).ctx ->
    Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
    Unchecked_types.Unchecked_types(Kernel.Coh).ctx
    * Unchecked_types.Unchecked_types(Kernel.Coh).tm)
    Stdlib.ref

val exec : loop_fn:(unit -> unit) -> prog -> unit