Operation on function symbols of
nonlinear multiplication theory
Th.nl.
mk_mul, mk_expt n, mk_outl are the function symbols
representing Mult and Expt(n), respectively.get f returns the function symbol in Th.nl represented by f,
or raises Not_found. - The test
is_mult f (is_expt f) succeeds iff f
represents Mult (some Expt(n)).
d_expt f returns n if f represents Expt(n); otherwise
Not_found is raised.pp p fmt (op, al) pretty-prints the appliation of op to the
argument list al depending on the value of Pretty.flag. See
also Pretty.apply. It assumes applications to Expt(n) to be
unary, whereas Mult is considered to be an nary function
symbol.