package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

package dedukti

dedukti.api
- Api
  - Dep
  - Env
  - Errors
  - Files
  - Meta
    
    APP
    
    ENCODING
    
    LF
    
    MetaConfiguration
    
    PROD
  - Pp
    
    Default
    
    Make
    
    S
    
    Printer
    
    Sig
  - Processor
    
    CustomEnv
    
    Interface
    
    MakeDependencies
    
    E
    
    MakeEntryPrinter
    
    E
    
    MakeSignatureBuilder
    
    E
    
    MakeTypeChecker
    
    E
    
    Registration
    
    S
    
    T
dedukti.kernel
- Kernel
  - Ac
  - Basic
    
    Debug
    
    LList
  - Confluence
  - Dtree
  - Exsubst
    
    ExSubst
  - Matching
    
    Make
    
    R
    
    Matcher
    
    Reducer
  - Reduction
    
    ConvChecker
    
    Default
    
    Make
    
    C
    
    M
    
    S
  - Rule
  - Signature
  - Srcheck
    
    SRChecker
    
    R
  - Subst
  - Term
  - Typing
    
    Default
    
    Make
    
    R
    
    S
  - Version
dedukti.parsers
- Parsers
  - Entry
  - Lexer
  - Menhir_parser
  - Parser
  - Preterm
  - Scoping
  - Tokens

Legend:
Library
Module
Module type
Parameter
Class
Class type

type files_error =

| ModuleNotFound of Kernel.Basic.mident
| MultipleModules of string * string list
| ObjectFileNotFound of Kernel.Basic.mident

exception Files_error of files_error

val add_path : string -> unit

add_path p add the p to the load path

val get_path : unit -> string list

get_path () returns all the paths in the load path

val find_object_file : Kernel.Basic.loc -> Kernel.Basic.mident -> string

get_find_object_file lc md returns the path assoiated to the module md or raise an exception

val object_file_of_input : Parsers.Parser.input -> string

object_file_of_input returns the filename associated to the input

val get_file : Kernel.Basic.mident -> string

get_file md returns the path associated to module md

val find_dk : 
  ignore:bool ->
  Kernel.Basic.mident ->
  string list ->
  string option

find_dk md path looks for the ".dk" file corresponding to the module named name in the directories of path. If no corresponding file is found, or if there are several possibilities, the program fails with a graceful error message.