On 21/03/17 08:35, Ralf Hemmecke wrote:
On 03/21/2017 09:26 AM, Martin Baker wrote:What I'm trying to say is that in, say, intuitionistic logic we have variables (in the mathematical sense - can range over all values). For example, proposition("a") here:(1) -> proposition("a") /\ logicT() (1) a Type : ILogic (2) -> proposition("a") /\ logicF() (2) _|_ Type : ILogic I don't think it would be correct for this to return 'false'.Exactly. Because 'false' is not an element of ILogic. Interestingly, even here you export logicF, logicT instead of relying on the functions/constants T and _|_ whose signatures you get from BoundetMeetSemilattice and BoundedJoinSemilattisc.
Yes, in a ideal world (and I agree existing code is not ideal) I think that T and _|_ (or unicode equivalent) should be used for both input and output. This is because 'top' and 'bottom' could be variable/proposition names but T and _|_ are less likely to be.
Martin B -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
