Bas Spitters (Aug 17 2020 at 11:33): Bas Spitters (Aug 17 2020 at 11:33):There is a theory for rationals within the reals. Is there a similar theory and hints database for the integers?
https://coq.inria.fr/library/Coq.QArith.Qreals.html
@Vincent Semeria ?
Bas Spitters (Aug 17 2020 at 11:49):Found it, but the rewrite database seems to be absent:
https://github.com/coq/coq/blob/master/theories/Reals/RIneq.v
Vincent Semeria (Aug 17 2020 at 11:55):I have never used hints or proof automation. What do you want to do with those theorems in RIneq ?
Bas Spitters (Aug 17 2020 at 12:19):In general, to write proofs in Coq with the convenient of proving theorems on paper.
Last updated: Jun 10 2023 at 23:01 UTC