package dedukti

  1. Overview
  2. Docs
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 =
  1. | PreType of Kernel.Basic.loc
  2. | PreId of Kernel.Basic.loc * Kernel.Basic.ident
  3. | PreQId of Kernel.Basic.loc * Kernel.Basic.name
  4. | PreApp of preterm * preterm * preterm list
  5. | PreLam of Kernel.Basic.loc * Kernel.Basic.ident * preterm option * preterm
  6. | PrePi of Kernel.Basic.loc * Kernel.Basic.ident option * preterm * preterm
val pp_preterm : Format.formatter -> preterm -> unit
type prepattern =
  1. | PCondition of preterm
  2. | PPattern of Kernel.Basic.loc * Kernel.Basic.mident option * Kernel.Basic.ident * prepattern list
  3. | PLambda of Kernel.Basic.loc * Kernel.Basic.ident * prepattern
  4. | PJoker of Kernel.Basic.loc * prepattern list
  5. | PApp of prepattern list
val pp_prepattern : Format.formatter -> prepattern -> unit
val clean_pre_pattern : prepattern -> prepattern
type pdecl = (Kernel.Basic.loc * Kernel.Basic.ident) * preterm option
val pp_pdecl : Format.formatter -> pdecl -> unit
type pcontext = pdecl list
val pp_pcontext : Format.formatter -> pcontext -> unit
val pp_prule : Format.formatter -> prule -> unit
OCaml

Innovation. Community. Security.