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 `Export.Rawdk`Source

Translate the parser-level AST to Dedukti.

Sourceval raw_ident : string Lplib.Base.pp

Sourceval ident : Parsing.Syntax.p_ident Lplib.Base.pp

Sourceval qident : Parsing.Syntax.p_qident Lplib.Base.pp

Sourceval param_id : Parsing.Syntax.p_ident option Lplib.Base.pp

Sourceval term : Parsing.Syntax.p_term Lplib.Base.pp

Source

val let_typ : 
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term Lplib.Base.pp

Source

val let_dfn : 
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term Lplib.Base.pp

Sourceval pterm : Parsing.Syntax.p_term Lplib.Base.pp

Sourceval terms : Parsing.Syntax.p_term array Lplib.Base.pp

Source

val param : 
  Parsing.Syntax.p_term option ->
  string ->
  Parsing.Syntax.p_ident option Lplib.Base.pp

Sourceval params : string -> Parsing.Syntax.p_params Lplib.Base.pp

Sourceval params_list : string -> Parsing.Syntax.p_params list Lplib.Base.pp

Sourceval abs : Parsing.Syntax.p_params list Lplib.Base.pp

Sourceval prod : Parsing.Syntax.p_params list Lplib.Base.pp

Sourceval arg : Parsing.Syntax.p_params list Lplib.Base.pp

Sourceval typ : Parsing.Syntax.p_term Lplib.Base.pp

Sourceval bool : bool Lplib.Base.pp

Sourceval assertion : (bool * Parsing.Syntax.p_assertion) Lplib.Base.pp

Sourceval strat : Core.Eval.strat Lplib.Base.pp

Sourceval query : Parsing.Syntax.p_query Lplib.Base.pp

Source

val remove_wraps : 
  Parsing.Syntax.p_term_aux Common.Pos.loc ->
  Parsing.Syntax.p_term_aux Common.Pos.loc

Sourceval rule : Parsing.Syntax.p_rule Lplib.Base.pp

Source

type modifiers =
  Core.Term.prop list
  * Core.Term.expo list
  * Core.Term.match_strat list
  * Parsing.Syntax.p_modifier_aux list

Sourceval partition_modifiers : Parsing.Syntax.p_modifier list -> modifiers

Source

val modifiers : 
  Parsing.Syntax.p_term option ->
  Parsing.Syntax.p_modifier list Lplib.Base.pp

Source

val get_ac_typ : 
  Common.Pos.popt ->
  modifiers ->
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term option ->
  Parsing.Syntax.p_term option

Sourceval command : Parsing.Syntax.p_command Lplib.Base.pp

Sourceval ast : Parsing.Syntax.ast Lplib.Base.pp

Sourceval print : Parsing.Syntax.ast -> unit

package lambdapi

Module Export.RawdkSource

Module `Export.Rawdk`Source