Waldek Hebisch <hebi...@math.uni.wroc.pl> writes:
[...]
| Note1: AFAICS OpenAxiom original in coercion to OutputForm is
| missing cases for false and true, which leads to infinite recursion.
| I added them to translation.
Thanks, I fixed it differently:
primaryFormula(p: %): OutputForm ==
p' := rep p
p' case T => p'@T::OutputForm
case constantIfCan p' is
c@Identifier => c::OutputForm
otherwise =>
is?(p', IMP) or is?(p', EQV) =>
args := argument p'
elt(operator(p')::OutputForm,
[formula first args, formula second args])$OutputForm
paren(formula p)$OutputForm
| Note2: I have no idea if/how the construct:
|
| false == per constantKernel FALSE
| true == per constantKernel TRUE
|
| works in OpenAxiom.
Yes, it does. I would prefer them to be known to the symbolic
expression machinery as constants, that is why I did not use this form:
| Instead I represent true and false as 0 argument operators.
|
| Note3: FriCAS instead of Pair has Product domain, I did relevant
| renamings.
|
| Note4: Because FriCAS parser performs transformations of 'not',
| 'and' and 'or' they are not usable as functions names. I replaced
| them by 'lnot', 'land' and 'lor'.
I would have thought that in that case, you would just use the existing
operators ~, /\, and \/. It has the benefit of implementing the missing
lattice operators, and or remaining compatible (from the user's perpective)
to the original OpenAxiom library it started from.
-- Gaby
------------------------------------------------------------------------------
All the data continuously generated in your IT infrastructure contains a
definitive record of customers, application performance, security
threats, fraudulent activity and more. Splunk takes this data and makes
sense of it. Business sense. IT sense. Common sense.
http://p.sf.net/sfu/splunk-d2d-oct
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
