Michael Norrish comments

Results 238 comments of


                                            Michael Norrish

Implement basic regex search functionality for DB.find

Exporting both `translate_regexp` and `parse_regexp` along with your own type seems perfectly reasonable to me. (And you're quite right about your `~` example; brain fade on my part.)

Implement basic regex search functionality for DB.find

Could you put the `datatype` declaration for `search_regexp` into the signature please? Having it be completely opaque with just a `type` declaration makes it difficult/impossible to do anything with it.

Implement basic regex search functionality for DB.find

Yes, that's right. You can avoid the "code smell" by declaring the datatype in a `structure` (a `.sml` file conventionally), and then referring to that declaration in both the signature...

Implement basic regex search functionality for DB.find

Thanks for your work on this!

Implement basic regex search functionality for DB.find

`DB.find "and~cl"` now goes into an infinite loop; do you have time to look into this?

Add simplification for bool_equality stuff.

Why is this a good idea? If anything, I'd prefer to simplify the LHS above into `B ==> ~A`.

Add simplification for bool_equality stuff.

(Which we could do by extending the implication congruence rule to assume the negation of the r.h.s. of the arrow while simplifying the left.)

Add simplification for bool_equality stuff.

Lots of it, it would appear! I'd be tempted to put `BOOL_EQ_IMP_CONV` into `bool_ss`.

[listSimps] Improved LIST_EQ_SIMP_CONV knowing SNOC

Thanks!

REABBREV_TAC renames duplicate abbreviations

It's not clear to me that this is a problematic behaviour.