Do use the explicit stack for term printing (except perhaps for printing sorts)

vprover / vampire

The Vampire Theorem Prover

https://vprover.github.io/

Other

302 stars 52 forks source link

Do use the explicit stack for term printing (except perhaps for printing sorts) #569

Closed quickbeam123 closed 5 months ago

quickbeam123 commented 5 months ago

direct printing only for sorts (and not vice versa); fixes #567

ibnyusuf commented 5 months ago

It's been that long, that I don't recall what the purpose of the negation was! That being said it clearly was related to the printing of higher-order sorts, so I think we can safely ignore since the printing of higher-order terms completely changes on the current HOL branch ahmed-new-hol.

In short, make printing work for first-order and we can worry about higher-order at the point of merge.