On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
exception AppliedGuardedTerm of Kernel.Basic.locexception BetaRedexInLHS of Kernel.Basic.locPreTerms
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 -> unittype 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 -> unitval clean_pre_pattern : prepattern -> prepatterntype pdecl = (Kernel.Basic.loc * Kernel.Basic.ident) * preterm optionval pp_pdecl : Stdlib.Format.formatter -> pdecl -> unittype pcontext = pdecl listval pp_pcontext : Stdlib.Format.formatter -> pcontext -> unittype prule =
Kernel.Basic.loc
* (Kernel.Basic.mident option * Kernel.Basic.ident) option
* pdecl list
* Kernel.Basic.mident option
* Kernel.Basic.ident
* prepattern list
* pretermval pp_prule : Stdlib.Format.formatter -> prule -> unitOn This Page