Create new function/constant/variable from string.

nick8325 / jukebox

A theorem prover

BSD 3-Clause "New" or "Revised" License

13 stars 0 forks source link

Create new function/constant/variable from string. #4

Closed jparsert closed 6 years ago

jparsert commented 6 years ago

So essentially I have a variable name and I extract the string of the variable and convert this string to lower case. Note, that the variable stays the same, I just now so happen to have a new string but with all lower cases. Now I would like to create (constant) function of that name. How would I do that? the code in question is: https://pastebin.com/m8pdgL3A In the general setting i essentially want to substitute all occurrences of the a variable with the newly generated constant of the almost same name. so if i have "! [A] : P(A)" I want to turn into "P(a)" where the quantifier is elminiated and the quantified variable is replaced by a constant.

nick8325 commented 6 years ago

I would recommend not using Fixed as that way you risk name clashes.

The way I would do it is to use variant: nameToLower f = variant (map toLower (base f)) [f].

This creates a name whose string value is by default map toLower (base f), but f is still part of the internal representation of the name so that in case of name clashes it will be renamed correctly.