package universo

You can search for identifiers within the package.

in-package search v0.2.0

package universo

universo.api
- Universo_api
universo.checking
- Checking
  - Checker
    
    MakeRE
    
    Conv
    
    RE
    
    Typing
universo.common
- Common
  - Constraints
  - Files
  - Log
  - Logic
    
    LRA_REIFICATION
    
    LRA_SPECIFICATION
    
    MakeLraSpecif
    
    Lra
    
    QFUF_SPECIFICATION
  - Oracle
    
    Util
  - Universes
    
    C
universo.elaboration
- Elaboration
  - Elaborate
  - Var
universo.solving
- Solving
  - Solver
    
    Make
    
    S
    
    MakeUF
    
    S
  - Utils
    
    LOGIC
    
    SMTSOLVER
    
    SOLVER
  - Z3arith
    
    Make
    
    Spec
  - Z3cfg
    
    Arith
    
    S
    
    Make
    
    ZL
    
    Syn
    
    Z3LOGIC
  - Z3syn

Legend:
Library
Module
Module type
Parameter
Class
Class type

module B = Kernel.Basic

module T = Kernel.Term

module type LRA_REIFICATION = sig ... end

type z =

| Z

type 'a s =

| S

type ('a, _) op =

| True : 'a -> ('a, z) op
| False : 'a -> ('a, z) op
| Zero : 'a -> ('a, z) op
| Succ : 'a -> ('a, z s) op
| Minus : 'a -> ('a, z s) op
| Eq : 'a -> ('a, z s s) op
| Max : 'a -> ('a, z s s) op
| IMax : 'a -> ('a, z s s) op
| Le : 'a -> ('a, z s s) op
| Ite : 'a -> ('a, z s s s) op

type ('a, 'b) arrow =

| Zero : 'b -> (z, 'b) arrow
| One : ('b -> 'b) -> (z s, 'b) arrow
| Two : ('b -> 'b -> 'b) -> (z s s, 'b) arrow
| Three : ('b -> 'b -> 'b -> 'b) -> (z s s s, 'b) arrow

type ('a, 'c) k = {

mk : 'b. ('a, 'b) op -> ('b, 'c) arrow;

}

module type LRA_SPECIFICATION = sig ... end

module MakeLraSpecif (Lra : LRA_REIFICATION) : LRA_SPECIFICATION

type theory = (Universes.pred * bool) list

module type QFUF_SPECIFICATION = sig ... end