Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type ac_ident = Basic.name * Term.algebraval pp_ac_ident : ac_ident Basic.printerval force_flatten_AC_term :
(Term.term -> Term.term) ->
(Term.term -> Term.term -> bool) ->
ac_ident ->
Term.term ->
Term.term listforce_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 listval flatten_AC_term : Basic.name -> Term.term -> Term.term list