vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

FDI is really not very good and not type-safe. #555

Open MichaelRawson opened 3 months ago

MichaelRawson commented 3 months ago

I played around with function definition introduction some time back. It was all fun and games and then it got merged into master because it seems to help sometimes. I didn't really think about sorts, or efficiency particularly. Now it is very buggy, see #542. Let this be a lesson to others!

I should probably Just Do It Better. Filing this to track progress.