package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

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 `Matching.Make`Source

This is the default implementation. * It relies on the provided : * - whnf reduction strategy to flatten AC terms without digging to deep inside * - snf reduction strategy to perform higher order matching when necessary * - are_convertible convertibility test

Parameters

module R : Reducer

Signature

Source

val solve_problem : 
  Rule.rule_name ->
  Signature.t ->
  (int -> Term.term Lazy.t) ->
  (int -> Term.term Lazy.t list) ->
  Dtree.pre_matching_problem ->
  Term.term Lazy.t Basic.LList.t option

solve_problem sg eq_conv ac_conv pb solves the pb matching problem using the given functions to convert positions in the stack to actual (lazy) terms.

package dedukti

Module Matching.MakeSource

Parameters

Signature

Module `Matching.Make`Source