package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

PreTerms

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.Preterm`Source

Sourceexception AppliedGuardedTerm of Kernel.Basic.loc

Sourceexception BetaRedexInLHS of Kernel.Basic.loc

PreTerms

This module defines structures representing terms before their scoping. That is to say before variables are scoped with De Bruijn indices

Sourcetype preterm =

| PreType of Kernel.Basic.loc
| PreId of Kernel.Basic.loc * Kernel.Basic.ident
| PreQId of Kernel.Basic.loc * Kernel.Basic.name
| PreApp of preterm * preterm * preterm list
| PreLam of Kernel.Basic.loc * Kernel.Basic.ident * preterm option * preterm
| PrePi of Kernel.Basic.loc * Kernel.Basic.ident option * preterm * preterm

Sourceval pp_preterm : Format.formatter -> preterm -> unit

Sourcetype prepattern =

| PCondition of preterm
| PPattern of Kernel.Basic.loc * Kernel.Basic.mident option * Kernel.Basic.ident * prepattern list
| PLambda of Kernel.Basic.loc * Kernel.Basic.ident * prepattern
| PJoker of Kernel.Basic.loc * prepattern list
| PApp of prepattern list

Sourceval pp_prepattern : Format.formatter -> prepattern -> unit

Sourceval clean_pre_pattern : prepattern -> prepattern

Sourcetype pdecl = (Kernel.Basic.loc * Kernel.Basic.ident) * preterm option

Sourceval pp_pdecl : Format.formatter -> pdecl -> unit

Sourcetype pcontext = pdecl list

Sourceval pp_pcontext : Format.formatter -> pcontext -> unit

type prule =
  Kernel.Basic.loc
  * (Kernel.Basic.mident option * Kernel.Basic.ident) option
  * pdecl list
  * Kernel.Basic.mident option
  * Kernel.Basic.ident
  * prepattern list
  * preterm

Sourceval pp_prule : Format.formatter -> prule -> unit