search

tsoding / Noq

Simple expression transformer that is not Coq.
MIT License
253 stars 24 forks source link

Replacing name of a functor turns it into a symbol #1

Closed rexim closed 2 years ago

rexim commented 2 years ago 
noq> shape f(a, b, c)
shaping f(a, b, c)
> apply rule f = g
 => g
> done
noq>
rexim commented 2 years ago

Oh, it's actually by design. f is recognized as a variable that matches the whole expression. This is confusing nonetheless.

rexim commented 2 years ago

We can resolve the confusion by introducing a special kind of expressions "variable" and use it for binding the sub-expressions instead of symbols. And match the symbols literally.

The variables can be denoted by capitalizing first character of the name. Similar to how Prolog does it.