package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

package dedukti

dedukti
- Library dedukti.api
  - Api
    
    Dep
    
    Env
    
    HName
    
    Errors
    
    Files
    
    Meta
    
    ENCODING
    
    PROD
    
    LF
    
    APP
    
    MetaConfiguration
    
    Pp
    
    Sig
    
    Printer
    
    Make
    
    Default
    
    Processor
    
    Interface
    
    S
    
    Registration
    
    T
    
    CustomEnv
    
    HName
    
    MakeTypeChecker
    
    MakeSignatureBuilder
    
    MakeEntryPrinter
    
    MakeDependencies
- Library dedukti.kernel
  - Kernel
    
    Ac
    
    Basic
    
    MidentSet
    
    IdentSet
    
    NameSet
    
    LList
    
    Debug
    
    Confluence
    
    Dtree
    
    Exsubst
    
    ExSubst
    
    Matching
    
    Reducer
    
    Matcher
    
    Make
    
    Reduction
    
    ConvChecker
    
    S
    
    Make
    
    Default
    
    Rule
    
    Signature
    
    Srcheck
    
    SRChecker
    
    Subst
    
    Term
    
    Typing
    
    S
    
    Make
    
    Default
    
    Version
- Library dedukti.parsers
  - Parsers
    
    Entry
    
    Lexer
    
    Menhir_parser
    
    Parser
    
    Preterm
    
    Scoping
    
    Tokens
- Sources
  - dedukti.api
    
    api.ml
    
    dep.ml
    
    env.ml
    
    errors.ml
    
    files.ml
    
    meta.ml
    
    pp.ml
    
    processor.ml
  - dedukti.kernel
    
    ac.ml
    
    basic.ml
    
    confluence.ml
    
    dtree.ml
    
    exsubst.ml
    
    kernel.ml
    
    matching.ml
    
    reduction.ml
    
    rule.ml
    
    signature.ml
    
    srcheck.ml
    
    subst.ml
    
    term.ml
    
    typing.ml
    
    version.ml
  - dedukti.parsers
    
    entry.ml
    
    lexer.ml
    
    menhir_parser.ml
    
    parser.ml
    
    parsers.ml
    
    preterm.ml
    
    scoping.ml
    
    tokens.ml

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

Module `Parsers.Scoping`Source

Sourceexception Scoping_error of Kernel.Basic.loc * string

Scope managmement: from preterms to terms.

Source

val scope_term : 
  Kernel.Basic.mident ->
  Kernel.Term.typed_context ->
  Preterm.preterm ->
  Kernel.Term.term

Source

val scope_rule : 
  Kernel.Basic.mident ->
  Preterm.prule ->
  Kernel.Rule.partially_typed_rule

package dedukti

Module Parsers.ScopingSource

Module `Parsers.Scoping`Source