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

Proper TH1 translation of ^[X: $tType]: ... #30

Closed lex-lex closed 7 years ago

lex-lex commented 8 years ago

At the moment, this is translated as /. .... but this is incorrect as the original statement is actual syntactic sugar for /. .... = /\ $true. This needs to be fixed.

lex-lex commented 7 years ago

Included since dcd593db9d027598fae81f7c65339e4c72cfbdcd