Hi all, I'm looking at some of the Light source code, and curious about some of the design decisions.
For example, this seems straightforward enough, given F: let NOT_DEF = new_basic_definition `(~) = \p. p ==> F`;; ... but on the face of it, it would seem even simpler to have done let NOT_DEF = new_basic_definition `(~) = \p. p <=> F`;; Is there a reason implication was chosen over equality for this definition? And this one I'm also not clear about: let F_DEF = new_basic_definition `F = !p:bool. p`;; falsehood is defined as "all propositions are true"... which is certainly false, though on the face of it would seem a little roundabout... does it have some particular felicitous properties, or is it just a case of it being the simplest way to define false given lambda and equals as primitives? Is there any documentation anywhere on the reasoning behind these decisions? ------------------------------------------------------------------------------ Free Software Download: Index, Search & Analyze Logs and other IT data in Real-Time with Splunk. Collect, index and harness all the fast moving IT data generated by your applications, servers and devices whether physical, virtual or in the cloud. Deliver compliance at lower cost and gain new business insights. http://p.sf.net/sfu/splunk-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
