search

JacquesCarette / hol-light-qe

The HOL Light theorem prover (moved from Google code)
Other
7 stars 1 forks source link

Hole fix #25

Closed sjjs7 closed 4 years ago

sjjs7 commented 4 years ago

Mostly fixed up the implementation of hole in fusion and changed how a hole is printed (it now prints its intended type as well). Also took the type argument away from quote.

wmfarmer commented 4 years ago

By mistake I approved the changes thrice.

The changes all look fine to me. I do have questions about some of Patrick's code that you didn't change.

The functions makeUnquoteQuote and UNQUOTE should be renamed, say, to absorbFilledHoles and HOLE_ABSORPTION.

sjjs7 commented 4 years ago

Oh yes I meant to do that! Thanks

On Thu., Jul. 2, 2020, 10:06 p.m. William M. Farmer, < notifications@github.com> wrote:

By mistake I approved the changes thrice.

The changes all look fine to me. I do have questions about some of Patrick's code that you didn't change.

The functions makeUnquoteQuote and UNQUOTE should be renamed, say, to absorbFilledHoles and HOLE_ABSORPTION.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/JacquesCarette/hol-light-qe/pull/25#issuecomment-653295137, or unsubscribe https://github.com/notifications/unsubscribe-auth/APPK65GN7MTPUHFWCLCO4J3RZU4LZANCNFSM4OPG4F6Q .

wmfarmer commented 4 years ago

I forgot to say that this is really good work. You are making significant progress.