package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

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 ac_ident = Basic.name * Term.algebra

val ac_ident_eq : ac_ident -> ac_ident -> bool

val pp_ac_ident : ac_ident Basic.printer

val force_flatten_AC_term : 
  (Term.term -> Term.term) ->
  (Term.term -> Term.term -> bool) ->
  ac_ident ->
  Term.term ->
  Term.term list

force_flatten_AC_term snf are_convertible aci t returns the list t1 ; ... ; tn where t is convertible with t1 + ... + tn and aci represents the AC(U) operator + while whnf is used to reduce to head normal form to check for + symbol at the head. All ti are reduced with whnf. are_convertible checks convertibility to neutral element if needed.

val flatten_AC_terms : Basic.name -> Term.term list -> Term.term list

val flatten_AC_term : Basic.name -> Term.term -> Term.term list

val unflatten_AC : ac_ident -> Term.term list -> Term.term