package dolmen_type

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package dolmen_type

dolmen_type
- Dolmen_type
  - Arith
    
    Smtlib2
    
    Int
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Real
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Real_Int
    
    Tff
    
    T
    
    Int
    
    Real
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Tptp
    
    Tff
    
    T
    
    Int
    
    Rat
    
    Real
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Arrays
    
    Smtlib2
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Base
  - Bitv
    
    Smtlib2
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Core
    
    Ae
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Smtlib2
    
    Tff
    
    T
    
    Tag
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Tptp
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Zf
    
    Tff
    
    Tag
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Def
    
    Declare
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Subst
    
    T
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Subst_arg
  - Float
    
    Smtlib2
    
    Tff
    
    T
    
    Bitv
    
    Float
    
    Real
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Logic
    
    Smtlib2
  - Misc
    
    Bitv
    
    Fuzzy_Hashtbl
    
    Fuzzy_Map
    
    Lists
    
    Options
    
    Strings
  - Strings
    
    Smtlib2
    
    Tff
    
    T
    
    String
    
    RegLan
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Tff
    
    Make
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Tff_intf
    
    S
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var

Legend:
Library
Module
Module type
Parameter
Class
Class type

Builtins for smtlib's core theory

Parameters

module Type : Tff_intf.S

module Tag : 
  Dolmen.Intf.Tag.Smtlib_Base
    with type 'a t = 'a Type.Tag.t
     and type term := Type.T.t

module Ty : Dolmen.Intf.Ty.Smtlib_Base with type t = Type.Ty.t

module T : 
  Dolmen.Intf.Term.Smtlib_Base
    with type t = Type.T.t
     and type cstr := Type.T.Cstr.t

Signature

val parse : Dolmen.Smtlib2.version -> Type.builtin_symbols