Improved TFX and THF support

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics

http://inf.fu-berlin.de/~lex/leo3

BSD 3-Clause "New" or "Revised" License

41 stars 10 forks source link

Closed lex-lex closed 2 years ago

lex-lex commented 2 years ago

Leo-III now contains experimental support for conditional expressions ($ite) and let expressions ($let) in TFX; and also for let expressions in THF.