package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a subs = private
  1. | ESID of int
  2. | CONS of 'a array * 'a subs
  3. | SHIFT of int * 'a subs
  4. | LIFT of int * 'a subs
val subs_id : int -> 'a subs
val subs_cons : ('a array * 'a subs) -> 'a subs
val subs_shft : (int * 'a subs) -> 'a subs
val subs_lift : 'a subs -> 'a subs
val subs_liftn : int -> 'a subs -> 'a subs
val subs_shift_cons : (int * 'a subs * 'a array) -> 'a subs
val expand_rel : int -> 'a subs -> (int * 'a, int * int option) Util.union
val is_subs_id : 'a subs -> bool
val comp : (('a subs * 'a) -> 'a) -> 'a subs -> 'a subs -> 'a subs
type lift = private
  1. | ELID
  2. | ELSHFT of lift * int
  3. | ELLFT of int * lift
val el_id : lift
val el_shft : int -> lift -> lift
val el_liftn : int -> lift -> lift
val el_lift : lift -> lift
val reloc_rel : int -> lift -> int
val is_lift_id : lift -> bool
val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs