package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

PreTerms

An implementation of The Lambda-Pi Modulo Theory

Install

dune-project

Dependency

github.com Readme Changelog Edit opam file Versions (2)

Authors

D

dedukti-dev@inria.fr

Maintainers

D

dedukti-dev@inria.fr

Sources

v2.7.tar.gz

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/dedukti.parsers/Parsers/Preterm/index.html

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

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