search

kframework / matching-logic-prover

15 stars 4 forks source link

Replace `\hole()` with `#hole` #49

Open h0nzZik opened 4 years ago

h0nzZik commented 4 years ago

This:

syntax Pattern ::= Int
...
| "\\hole" "(" ")" [klabel(Phole)]

is a conceptual duplication of

syntax Variable ::= "#hole"

(from https://github.com/kframework/matching-logic-prover/blob/master/prover/lang/kore-lang.md)

nishantjr commented 4 years ago

~Any reason that this is not a variable?~ nevermind. I misunderstood

xc93 commented 4 years ago

Adding this: rule #hole => \\hole()?

nishantjr commented 4 years ago

\hole() looks more like a symbol than a variable. I think replacing all instances of \hole() with #hole makes sense? We may need to change #hole to a set variable depending on how we use it of course

h0nzZik commented 4 years ago

I have been thinking of completely removing \hole() and use only #hole.