package universo

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

module B = Kernel.Basic

module F = Files

module R = Kernel.Rule

module S = Kernel.Signature

module T = Kernel.Term

module U = Universes

module M = Api.Meta

type t = {

}

type print_cstrs = {

}

val dummy_name : R.rule_name

val mk_rule : Kernel.Basic.name -> Kernel.Basic.name -> 'a R.rule

val print_rule : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  ('a * 'a) ->
  unit

val print_eq_var : 
  Format.formatter ->
  (Kernel.Basic.name * Kernel.Basic.name) ->
  unit

val print_predicate : Format.formatter -> U.pred -> unit

val mk_var_cstr : 
  (B.name -> B.name -> 'a) ->
  B.name ->
  B.name ->
  B.name * B.name

mk_var_cstre env f l r add the constraint l =?= r. Call f on l and r such that l >= r.

val deps : B.mident list ref

val mk_cstr : t -> (B.name -> B.name -> 'a) -> U.cstr -> bool

val get_deps : unit -> B.mident list

val flush : unit -> unit