package logtk

You can search for identifiers within the package.

in-package search v0.2.0

logtk
- Library logtk
  - Logtk
    
    Binder
    
    TPTP
    
    ZF
    
    Builtin
    
    Arith
    
    Map
    
    Set
    
    Tbl
    
    Tag
    
    TPTP
    
    ArithOp
    
    ZF
    
    Cnf
    
    Comparison
    
    PARTIAL_ORD
    
    Compute_prec
    
    Congruence
    
    S
    
    TERM
    
    Make
    
    FO
    
    Congruence_intf
    
    S
    
    DBEnv
    
    Defined_pos
    
    Fmt
    
    Arr
    
    Dtree
    
    Make
    
    E
    
    Default
    
    E
    
    FV_tree
    
    Make
    
    Feature_fun
    
    C
    
    FeatureVector
    
    T
    
    Make
    
    C
    
    Feature
    
    IntMap
    
    CSet
    
    Fingerprint
    
    Make
    
    Leaf
    
    FixpointUnif
    
    T
    
    US
    
    Flex_state
    
    HO_unif
    
    HVar
    
    Hash
    
    Hashcons
    
    HashedType
    
    S
    
    Make
    
    MakeNonWeak
    
    IArray
    
    ID
    
    Map
    
    Set
    
    Tbl
    
    Ind_ty
    
    Index
    
    LEAF
    
    MakeLeaf
    
    TERM_IDX
    
    CLAUSE
    
    SUBSUMPTION_IDX
    
    EQUATION
    
    BasicEquation
    
    UNIT_IDX
    
    Index_intf
    
    LEAF
    
    TERM_IDX
    
    Leaf
    
    CLAUSE
    
    SUBSUMPTION_IDX
    
    C
    
    EQUATION
    
    UNIT_IDX
    
    E
    
    InnerTerm
    
    I
    
    Map
    
    Set
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
    
    DB
    
    Seq
    
    Pos
    
    Input_format
    
    Interfaces
    
    EQ
    
    HASH
    
    ORD
    
    PRINT
    
    PRINT1
    
    PRINT2
    
    PRINT3
    
    PRINT_OVERLOAD
    
    PRINT_DE_BRUIJN
    
    ITER
    
    MONOID
    
    GROUP
    
    JPFull
    
    Make
    
    JP_unif
    
    T
    
    US
    
    S
    
    Lambda
    
    Inner
    
    LazyList
    
    Literal
    
    Set
    
    Comp
    
    Seq
    
    Pos
    
    View
    
    Conv
    
    Literals
    
    Seq
    
    Pos
    
    Conv
    
    View
    
    Multiset
    
    S
    
    Make
    
    Seq
    
    Multiset_intf
    
    S
    
    Seq
    
    Multisets
    
    MT
    
    Seq
    
    MMT
    
    Seq
    
    NPDtree
    
    Make
    
    E
    
    MakeTerm
    
    Leaf
    
    Options
    
    Ordering
    
    Output_format
    
    PUnif
    
    IntSet
    
    Make
    
    ParseLocation
    
    Infix
    
    PatternUnif
    
    US
    
    S
    
    Polynomial
    
    IntegerModule
    
    OrderedType
    
    S
    
    Make
    
    Position
    
    Map
    
    Build
    
    With
    
    Infix
    
    PragUnifParams
    
    Precedence
    
    Weight
    
    Infix
    
    Constr
    
    Seq
    
    PrefWeight
    
    S
    
    Make
    
    Proof
    
    Loc
    
    Tag
    
    Rule
    
    Kind
    
    Src
    
    Result
    
    Step
    
    Parent
    
    S
    
    Tbl
    
    Rewrite
    
    Term
    
    Rule
    
    Set
    
    Rule_inst_set
    
    Lit
    
    Rule
    
    Rule
    
    Rule_set
    
    Defined_cst
    
    SLiteral
    
    TPTP
    
    ZF
    
    STerm
    
    Set
    
    Map
    
    Tbl
    
    StringSet
    
    Seq
    
    TPTP
    
    TPTP_THF
    
    ZF
    
    StrMap
    
    Scoped
    
    Signal
    
    Signature
    
    Seq
    
    Skolem
    
    SolidSubsumption
    
    Make
    
    SolidUnif
    
    T
    
    US
    
    Make
    
    Statement
    
    Seq
    
    ZF
    
    TPTP
    
    Subst
    
    Renaming
    
    SPECIALIZED
    
    Ty
    
    FO
    
    Projection
    
    Term
    
    Classic
    
    IntMap
    
    Set
    
    Map
    
    Tbl
    
    VarSet
    
    VarMap
    
    VarTbl
    
    Seq
    
    Pos
    
    AC_SPEC
    
    AC
    
    Form
    
    Arith
    
    DB
    
    TPTP
    
    ZF
    
    Conv
    
    Type
    
    Set
    
    Map
    
    Tbl
    
    Seq
    
    VarSet
    
    VarMap
    
    VarTbl
    
    TPTP
    
    ZF
    
    Conv
    
    TypeInference
    
    TyBuiltin
    
    Ctx
    
    TypedSTerm
    
    Ty
    
    Form
    
    Set
    
    Map
    
    Tbl
    
    Seq
    
    Subst
    
    Var_tbl
    
    UStack
    
    TPTP
    
    TPTP_THF
    
    ZF
    
    Unif
    
    S
    
    Inner
    
    Ty
    
    FO
    
    UnifFramework
    
    S
    
    US
    
    LL
    
    T
    
    PARAMETERS
    
    S
    
    US
    
    Make
    
    Unif_constr
    
    FO
    
    Unif_intf
    
    S
    
    Unif_subst
    
    FO
    
    UntypedAST
    
    Loc
    
    T
    
    A
    
    Util
    
    Section
    
    Exn
    
    Flag
    
    Int_map
    
    Int_set
    
    Var
    
    Set
    
    Subst
    
    ZProf
- Library logtk.arith
  - Logtk_arith
    
    Z
    
    Q
- Library logtk.parsers
  - Logtk_parsers
    
    Ast_dk
    
    A
    
    T
    
    Set
    
    Map
    
    Tbl
    
    StringSet
    
    Seq
    
    TPTP
    
    TPTP_THF
    
    ZF
    
    StrMap
    
    Ast_tptp
    
    CallProver
    
    A
    
    Prover
    
    Eprover
    
    Lex_dk
    
    Lex_tptp
    
    Lex_zf
    
    Parse_dk
    
    Parse_tptp
    
    Parse_zf
    
    Parsing_utils
    
    Tip_ast
    
    Loc
    
    Tip_lexer
    
    A
    
    Loc
    
    Tip_parser
    
    Trace_tstp
    
    StepTbl
    
    Util_dk
    
    A
    
    Util_tip
    
    A
    
    Util_tptp
    
    A
    
    Util_zf
- Library logtk.proofs
  - Logtk_proofs
    
    LLProof
    
    Tbl
    
    Dot
    
    LLProof_check
    
    LLProof_conv
    
    LLProver
    
    LLTerm
    
    Int_op
    
    Rat_op
    
    LINEXP
    
    Linexp_int
    
    Linexp_rat
    
    Form
    
    Set
    
    Conv
- Library logtk.solving
  - Logtk_solving
    
    Lpo
    
    Constraint
    
    Seq
    
    Solution
    
    FO
    
    TypedSTerm
- Sources
  - logtk
    
    Binder.ml
    
    Builtin.ml
    
    Cnf.ml
    
    Comparison.ml
    
    Compute_prec.ml
    
    Congruence.ml
    
    Congruence_intf.ml
    
    DBEnv.ml
    
    Defined_pos.ml
    
    Dtree.ml
    
    FV_tree.ml
    
    FeatureVector.ml
    
    Fingerprint.ml
    
    FixpointUnif.ml
    
    Flex_state.ml
    
    HO_unif.ml
    
    HVar.ml
    
    Hash.ml
    
    Hashcons.ml
    
    IArray.ml
    
    ID.ml
    
    Ind_ty.ml
    
    Index.ml
    
    Index_intf.ml
    
    InnerTerm.ml
    
    Input_format.ml
    
    Interfaces.ml
    
    JPFull.ml
    
    JP_unif.ml
    
    Lambda.ml
    
    LazyList.ml
    
    Literal.ml
    
    Literals.ml
    
    Multiset.ml
    
    Multiset_intf.ml
    
    Multisets.ml
    
    NPDtree.ml
    
    Options.ml
    
    Ordering.ml
    
    Output_format.ml
    
    PUnif.ml
    
    ParseLocation.ml
    
    PatternUnif.ml
    
    Polynomial.ml
    
    Position.ml
    
    PragUnifParams.ml
    
    Precedence.ml
    
    PrefWeight.ml
    
    Proof.ml
    
    Rewrite.ml
    
    SLiteral.ml
    
    STerm.ml
    
    Scoped.ml
    
    Signature.ml
    
    Skolem.ml
    
    SolidSubsumption.ml
    
    SolidUnif.ml
    
    Statement.ml
    
    Subst.ml
    
    Term.ml
    
    Type.ml
    
    TypeInference.ml
    
    TypedSTerm.ml
    
    Unif.ml
    
    UnifFramework.ml
    
    Unif_constr.ml
    
    Unif_intf.ml
    
    Unif_subst.ml
    
    UntypedAST.ml
    
    Util.ml
    
    Var.ml
    
    ZProf.ml
    
    logtk.ml
    
    signal.ml
  - logtk.arith
    
    logtk_arith.ml
  - logtk.parsers
    
    Ast_dk.ml
    
    Lex_dk.ml
    
    Lex_tptp.ml
    
    Lex_zf.ml
    
    Parse_dk.ml
    
    Parse_tptp.ml
    
    Parse_zf.ml
    
    Tip_ast.ml
    
    Tip_lexer.ml
    
    Tip_parser.ml
    
    Util_dk.ml
    
    ast_tptp.ml
    
    callProver.ml
    
    logtk_parsers.ml
    
    parsing_utils.ml
    
    trace_tstp.ml
    
    util_tip.ml
    
    util_tptp.ml
    
    util_zf.ml
  - logtk.proofs
    
    LLProof.ml
    
    LLProof_check.ml
    
    LLProof_conv.ml
    
    LLProver.ml
    
    LLTerm.ml
    
    logtk_proofs.ml
  - logtk.solving
    
    logtk_solving.ml
    
    lpo.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Logtk_proofs.LLProof_conv`

val conv : Logtk.Proof.t -> LLProof.t