search

kframework / matching-logic-prover

15 stars 4 forks source link

`\typeof` construct, set variables #60

Closed h0nzZik closed 4 years ago

nishantjr commented 4 years ago

This looks good. Can you add a few test cases (perhaps just for the new cases) for #syntacticMatch. Last commit message should be something more descriptive perhaps: "kore: add cases for \typeof for various meta functions"

nishantjr commented 4 years ago

This looks good. Can you add a few test cases (perhaps just for the new cases) for #syntacticMatch. Last commit message should be something more descriptive perhaps: "kore: add cases for \typeof for various meta functions"

I guess in the long run, alphaRename, subst, hasImplicationContext etc should all be implemented as visitors?

nishantjr commented 4 years ago

This looks good. Can you add a few test cases (perhaps just for the new cases) for #syntacticMatch. Last commit message should be something more descriptive perhaps: "kore: add cases for \typeof for various meta functions"

I guess in the long run, alphaRename, subst, hasImplicationContext etc should all be implemented as visitors?

nishantjr commented 4 years ago

Looks good!