search

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
BSD 3-Clause "New" or "Revised" License
42 stars 10 forks source link

Type sharing #33

Closed lex-lex closed 7 years ago

lex-lex commented 8 years ago

Apply sharing for types as well. It seems that BaseTypeNodes (i.e. case classes for base types) are being produced at a high rate.

lex-lex commented 7 years ago

Implemented for ground types and bound type variables since a43f0ce3bab69604cb14e82270439259603b2f05 This should suffice.