package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

PreTerms

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

exception AppliedGuardedTerm of Kernel.Basic.loc

exception 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

type 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

val pp_preterm : Stdlib.Format.formatter -> preterm -> unit

type 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

val pp_prepattern : Stdlib.Format.formatter -> prepattern -> unit

val clean_pre_pattern : prepattern -> prepattern

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

val pp_pdecl : Stdlib.Format.formatter -> pdecl -> unit

type pcontext = pdecl list

val pp_pcontext : Stdlib.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

val pp_prule : Stdlib.Format.formatter -> prule -> unit