search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Term interface method for `observe (hnorm t)` #86

Closed robblanco closed 5 years ago

robblanco commented 7 years ago

Does it make sense to extend the Term interface with a method that performs a "canonical inspection" of terms, conflating head normalization and observe? We have spoken before about how this is a sort of standard, and it makes sense to me if the interface encourages this, and makes it explicit (and more compact).

chaudhuri commented 7 years ago

I am not sure hnorm needs to be exposed by Term, actually, so maybe observe can take over the function.

robblanco commented 7 years ago

What about Term.norm?

chaudhuri commented 7 years ago

As far as I can tell, that function isn't used anywhere in Abella.

robblanco commented 7 years ago

On this note, I was using norm in one of my experiments, but I don't think the code is even composable. In particular, it returns terms with Vars unprotected by Ptr.

chaudhuri commented 5 years ago

I think everything relevant to this issue has already been addressed long ago.