Dolmen_type.Arith.Zf · dolmen_type 0.7

dolmen_type

A typechecker for automated deduction languages

IN THIS PACKAGE

library dolmen_type
- module Dolmen_type
  - module Arith
    
    module Ae
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Int
    
    module Real
    
    module Smtlib2
    
    module Int
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Real
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Real_Int
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Int
    
    module Real
    
    module Tptp
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Int
    
    module Rat
    
    module Real
    
    module Zf
    
    module Thf
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Int
  - module Arrays
    
    module Ae
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Smtlib2
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
  - module Base
  - module Bitv
    
    module Ae
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Smtlib2
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
  - module Core
    
    module Ae
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Tag
    
    argument 3-Ty
    
    argument 4-T
    
    module Dimacs
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-T
    
    module Smtlib2
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Tag
    
    argument 3-Ty
    
    argument 4-T
    
    module Tptp
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Thf
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Const
    
    module Zf
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Tag
    
    argument 3-Ty
    
    argument 4-T
  - module Def
    
    module Declare
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    module Subst
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-T
    
    module type Subst_arg
  - module Float
    
    module Smtlib2
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module Bitv
    
    module Float
    
    module Real
  - module Intf
    
    module type Formulas
  - module Logic
    
    module Smtlib2
  - module Misc
    
    module Bitv
    
    module Lists
    
    module Options
    
    module Strings
  - module Strings
    
    module Smtlib2
    
    module Tff
    
    argument 1-Type
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
    
    argument 2-Ty
    
    argument 3-T
    
    module String
    
    module RegLan
  - module Tff
    
    module Make
    
    argument 1-Tag
    
    argument 2-Ty
    
    module Const
    
    module Var
    
    argument 3-T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
  - module Tff_intf
    
    module type S
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var
  - module Thf
    
    module Make
    
    argument 1-Tag
    
    argument 2-Ty
    
    module Const
    
    module Var
    
    argument 3-T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
  - module Thf_intf
    
    module type S
    
    module T
    
    module Const
    
    module Cstr
    
    module Field
    
    module Var
    
    module Tag
    
    module Ty
    
    module Const
    
    module Var

Module Dolmen_type . Arith . Zf

module Thf
  (Type : Thf_intf.S)
  (Ty : Dolmen.Intf.Ty.Zf_Arith with type t := Type.Ty.t)
  (T : Dolmen.Intf.Term.Zf_Arith with type t := Type.T.t) : 
  sig ... end

dolmen_type 0.7 0.6 0.5

dolmen_type