search

proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript
MIT License
8 stars 0 forks source link

Conflate Const and Var in Term #3

Closed phlegmaticprogrammer closed 10 years ago

phlegmaticprogrammer commented 10 years ago

Right now Vars and Consts have different constructors. This produces a problem when printing, because when a var has the same name as a constant, and the constant is referred to inside the context of the var, then this term cannot be printed without switching constant and var. So it seems that Vars and Consts should be really the same in the term such that this cannot happen. Or, alternatively, make terms illegal which behave like that.

phlegmaticprogrammer commented 10 years ago

After some thought I think that having different constructors for Consts and Vars is just too useful to give up. What this means for printing terms is that alpha-conversion has to take place during / before printing when a situation occurs where a constant name would be hidden by a variable name.

phlegmaticprogrammer commented 10 years ago

This has been resolved by doing alpha-conversion during printing if necessary.