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

Advanced walkthrough documentation [website] #100

Closed amerikan closed 6 years ago

amerikan commented 6 years ago

Not sure if this is the best channel to mention this, but....

I was going through the advanced walk through on the website, http://abella-prover.org/advanced-walkthrough.html There's a theorem referred as member_uniq.

At the very bottom there's a link to: http://abella-prover.org/examples/lambda-calculus/type-uniq/type-uniq.html On this page it is called as ctx_uniq.

It appears they're both the same exact thing. It threw me off for a bit. It would be good to just use one or the other for consistency.

chaudhuri commented 6 years ago

Thanks. This should now be fixed.