Currently, we match against the name of type classes like LE.le and replace them with corresponding SMT names like <. However, that is not always accurate as operators like < are overloaded for many types in Lean. Whereas = is the only overloaded operator in SMT-LIB. Other operators are not overloaded. For example, less than is represented by < for integers and str.< for strings. This PR addresses this issue by matching against the type class and its type arguments and maps that to the appropriate SMT-LIB function symbol.
Currently, we match against the name of type classes like
LE.leand replace them with corresponding SMT names like<. However, that is not always accurate as operators like<are overloaded for many types in Lean. Whereas=is the only overloaded operator in SMT-LIB. Other operators are not overloaded. For example, less than is represented by<for integers andstr.<for strings. This PR addresses this issue by matching against the type class and its type arguments and maps that to the appropriate SMT-LIB function symbol.