package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

libzipperposition
- Libzipperposition
  - AC
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - AC_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - BBox
    
    Lit
    
    Set
    
    Tbl
  - Bool_clause
  - Bool_lit
    
    Make
    
    Payload
    
    Set
    
    Tbl
    
    PAYLOAD
  - Bool_lit_intf
    
    S
    
    Set
    
    Tbl
  - Bool_selection
  - Classify_cst
  - Clause
    
    Make
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
  - ClauseContext
    
    Set
  - ClauseQueue
    
    Make
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    PriorityFun
    
    WeightFun
  - ClauseQueue_intf
    
    S
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    PriorityFun
    
    WeightFun
  - Clause_intf
    
    S
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
  - Combinators
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Combinators_base
  - Const
  - Cover_set
    
    Case
  - Ctx
    
    Key
    
    Make
    
    Lit
    
    X
    
    PARAMETERS
  - Ctx_intf
    
    S
    
    Lit
  - Cut_form
    
    FV_tbl
    
    X
    
    Pos
    
    Seq
  - Env
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    X
    
    Ctx
    
    Lit
  - Env_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Eprover_interface
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Extensions
  - FormulaRename
    
    Make
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
  - Ind_cst
    
    Cst_set
  - Lift_lambdas
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Params
  - ProofState
    
    Make
    
    ActiveSet
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - ProofState_intf
    
    S
    
    ActiveSet
    
    C
    
    ClauseSet
    
    Ctx
    
    Lit
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    Ctx
    
    Lit
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - SClause
    
    TPSet
  - Sat_solver
    
    Make
    
    S
  - Sat_solver_intf
    
    S
  - Saturate
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Selection
  - Signals
  - SimplM
    
    Infix
  - Stream
    
    ARG
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    Make
    
    A
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
  - StreamQueue
    
    ARG
    
    Stm
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    Make
    
    A
    
    Stm
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    WeightFun
  - StreamQueue_intf
    
    S
    
    Stm
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    WeightFun
  - Stream_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
  - Trail
libzipperposition.avatar
- Libzipperposition_avatar
  - Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    Sat
  - S
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    Solver
  - UnionFind
    
    Make
    
    P
    
    PAIR
libzipperposition.calculi
- Libzipperposition_calculi
  - App_encode
  - Bce
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Bce_pe_fixpoint
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Bool_encode
  - Booleans
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - EnumTypes
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Eq_encode
  - Fool
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Heuristics
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    PS
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Higher_order
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Hlt_elim
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Ind_types
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Lazy_cnf
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - MyHeap
    
    Make
    
    Elt
  - Pred_elim
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Pure_literal_elim
    
    IDMap
  - Qle
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Rewriting
    
    Make
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - Superposition
    
    Make
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    PS
    
    ActiveSet
    
    C
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
  - Superposition_intf
    
    S
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
    
    PS
    
    ActiveSet
    
    C
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
libzipperposition.induction
- Libzipperposition_induction
  - Make
    
    A
    
    Solver
    
    E
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
  - S
    
    Env
    
    C
    
    ClauseSet
    
    Eligible
    
    Pos
    
    Seq
    
    Tbl
    
    WithPos
    
    Ctx
    
    Lit
    
    FormRename
    
    Ctx
    
    Lit
    
    ProofState
    
    ActiveSet
    
    CLAUSE_SET
    
    CQueue
    
    C
    
    PriorityFun
    
    WeightFun
    
    PassiveSet
    
    SimplSet
    
    SubsumptionIndex
    
    C
    
    TermIndex
    
    Leaf
    
    UnitIndex
    
    E
    
    Stm
    
    Ctx
    
    Lit
    
    StmQ
    
    WeightFun
libzipperposition.phases
- Libzipperposition_phases
  - Phases
    
    Infix
    
    Key
  - Phases_impl

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Env : Libzipperposition.Env.S

val register : unit -> unit

Register the inference rules for inductive reasoning