Preterm (p.dedukti.2.7.doc.dedukti.parsers.Parsers.Preterm)

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

Source

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