David L. Rager comments

Results 178 comments of


                                            David L. Rager

Improve integration of SULFA into the community books

Agreed that it'd be nice to clean this up. Right now it's effectively just dead code. OTOH, we already have a bunch of "dead code" that's mostly only included for...

[defrule] Add output that says which runes were enabled manually but not used

_From [[email protected]](https://code.google.com/u/102895947197065323718/) on March 18, 2014 07:30:33_ Kaufmann and Wetzler recently added a tool that automatically sees what hyps aren't being used: tools/remove-hyps.lisp. As I clean up proofs, this is...

[defrule] Add output that says which runes were enabled manually but not used

Having another thought today that setting whether "defrule audit mode" is enabled should probably be done with a table event.

ash-natp-type

_From [[email protected]](https://code.google.com/u/102895947197065323718/) on January 28, 2014 17:33:07_ Ah, I admit I don't understand why the rule is written in terms of (not (and ...)), but that's probably just a tangential...

ash-natp-type

_From [[email protected]](https://code.google.com/u/102895947197065323718/) on January 28, 2014 17:57:32_ Of course, what I really want is (defrule ash-natp-type-oraclee (equal (natp (ash x y)) (natp x)) :enable natp) But that's just not true...

ash-natp-type

_From [[email protected]](https://code.google.com/u/[email protected]/) on January 28, 2014 18:04:58_ The original :type-prescription rule seems fine to me, what with its "type-like" hypotheses. If you produce an example showing what's wrong with it,...