package dedukti

  1. Overview
  2. Docs
type ac_ident = Basic.name * Term.algebra
val ac_ident_eq : ac_ident -> ac_ident -> bool
val pp_ac_ident : ac_ident Basic.printer
val force_flatten_AC_term : (Term.term -> Term.term) -> (Term.term -> Term.term -> bool) -> ac_ident -> Term.term -> Term.term list

force_flatten_AC_term snf are_convertible aci t returns the list t1 ; ... ; tn where t is convertible with t1 + ... + tn and aci represents the AC(U) operator + while whnf is used to reduce to head normal form to check for + symbol at the head. All ti are reduced with whnf. are_convertible checks convertibility to neutral element if needed.

val flatten_AC_terms : Basic.name -> Term.term list -> Term.term list
val flatten_AC_term : Basic.name -> Term.term -> Term.term list
val unflatten_AC : ac_ident -> Term.term list -> Term.term
OCaml

Innovation. Community. Security.