package lambdapi

You can search for identifiers within the package.

in-package search v0.2.0

package lambdapi

lambdapi
- CHANGES
- README
- Library lambdapi.common
  - Common
    
    Console
    
    State
    
    Debug
    
    D
    
    Error
    
    Escape
    
    Library
    
    LibMap
    
    Logger
    
    Path
    
    Path
    
    Set
    
    Map
    
    Pos
- Library lambdapi.core
  - Core
    
    Builtin
    
    Coercion
    
    Ctxt
    
    Env
    
    Eval
    
    Ghost
    
    Infer
    
    Inverse
    
    LibMeta
    
    LibTerm
    
    Print
    
    Sig_state
    
    Sign
    
    Term
    
    Raw
    
    Var
    
    VarSet
    
    VarMap
    
    Sym
    
    SymSet
    
    SymMap
    
    Meta
    
    MetaSet
    
    MetaMap
    
    Tree
    
    CP
    
    PSet
    
    CM
    
    Tree_type
    
    TC
    
    TCMap
    
    Unif
    
    Unif_rule
    
    Version
- Library lambdapi.export
  - Export
    
    Coq
    
    Qid
    
    QidMap
    
    Dk
    
    Hrs
    
    V
    
    VMap
    
    Rawdk
    
    Xtc
- Library lambdapi.handle
  - Handle
    
    Command
    
    Compile
    
    PureUpToSign
    
    Fol
    
    Inductive
    
    Proof
    
    Goal
    
    Query
    
    Rewrite
    
    Tactic
    
    Why3_tactic
- Library lambdapi.lplib
  - Lplib
    
    Array
    
    A
    
    Base
    
    Int
    
    Bytes
    
    B
    
    Color
    
    Extra
    
    IntMap
    
    IntSet
    
    StrMap
    
    StrSet
    
    Filename
    
    List
    
    L
    
    Option
    
    Monad
    
    Applicative
    
    Range
    
    RangeMap
    
    Make
    
    Range
    
    Range
    
    RangeMap_intf
    
    S
    
    Range
    
    Range_intf
    
    S
    
    String
    
    S
    
    B
    
    Uchar
- Library lambdapi.lsp
  - Lsp
    
    Lp_doc
    
    LSP
    
    Lp_lsp
    
    Lsp_base
    
    J
    
    Lsp_io
    
    F
    
    J
- Library lambdapi.parsing
  - Parsing
    
    DkBasic
    
    WS
    
    DkLexer
    
    DkParser
    
    DkRule
    
    DkTokens
    
    LpLexer
    
    LpParser
    
    Package
    
    Parser
    
    PARSER
    
    Lp
    
    Dk
    
    Pratt
    
    Pratt
    
    Pretty
    
    Scope
    
    SearchQuerySyntax
    
    Syntax
    
    P
- Library lambdapi.pure
  - Pure
    
    Command
    
    Tactic
    
    ProofTree
- Library lambdapi.tool
  - Tool
    
    External
    
    Indexing
    
    Lcr
    
    Sr
    
    Tree_graphviz
    
    Websearch
- Sources
  - lambdapi.common
    
    common.ml
    
    console.ml
    
    debug.ml
    
    error.ml
    
    escape.ml
    
    library.ml
    
    logger.ml
    
    path.ml
    
    pos.ml
  - lambdapi.core
    
    builtin.ml
    
    coercion.ml
    
    core.ml
    
    ctxt.ml
    
    env.ml
    
    eval.ml
    
    ghost.ml
    
    infer.ml
    
    inverse.ml
    
    libMeta.ml
    
    libTerm.ml
    
    print.ml
    
    sig_state.ml
    
    sign.ml
    
    term.ml
    
    tree.ml
    
    tree_type.ml
    
    unif.ml
    
    unif_rule.ml
    
    version.ml
  - lambdapi.export
    
    coq.ml
    
    dk.ml
    
    export.ml
    
    hrs.ml
    
    rawdk.ml
    
    xtc.ml
  - lambdapi.handle
    
    command.ml
    
    compile.ml
    
    fol.ml
    
    handle.ml
    
    inductive.ml
    
    proof.ml
    
    query.ml
    
    rewrite.ml
    
    tactic.ml
    
    why3_tactic.ml
  - lambdapi.lplib
    
    array.ml
    
    base.ml
    
    bytes.ml
    
    color.ml
    
    extra.ml
    
    filename.ml
    
    list.ml
    
    lplib.ml
    
    option.ml
    
    range.ml
    
    rangeMap.ml
    
    rangeMap_intf.ml
    
    range_intf.ml
    
    string.ml
    
    uchar.ml
  - lambdapi.lsp
    
    lp_doc.ml
    
    lp_lsp.ml
    
    lsp.ml
    
    lsp_base.ml
    
    lsp_io.ml
  - lambdapi.parsing
    
    dkBasic.ml
    
    dkLexer.ml
    
    dkParser.ml
    
    dkRule.ml
    
    dkTokens.ml
    
    lpLexer.ml
    
    lpParser.ml
    
    package.ml
    
    parser.ml
    
    parsing.ml
    
    pratt.ml
    
    pretty.ml
    
    scope.ml
    
    searchQuerySyntax.ml
    
    syntax.ml
  - lambdapi.pure
    
    pure.ml
  - lambdapi.tool
    
    external.ml
    
    indexing.ml
    
    lcr.ml
    
    sr.ml
    
    tool.ml
    
    tree_graphviz.ml
    
    websearch.ml

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

Module `Pure.Tactic`Source

Abstract representation of a tactic (proof item).

Sourcetype t

Sourceval equal : t -> t -> bool

Sourceval get_pos : t -> Common.Pos.popt

Sourceval print : t Lplib.Base.pp

package lambdapi

Module Pure.TacticSource

Module `Pure.Tactic`Source