Ignat Insarov (Jun 17 2021 at 15:04): Ignat Insarov (Jun 17 2021 at 15:04):I want to use Coq.QArith to compute something. Here is my code: <https://gist.github.com/kindaro/92a7d53a4c9a4297417310dcf0a599b7>. I cannot destruct or eliminate the proof of existence of the number I want to have computed. What do?
Gaëtan Gilbert (Jun 17 2021 at 15:06):use { (x: ℚ) | e₂ = Root 2 x} instead of ∃ (x: ℚ), e₂ = Root 2 x
Ignat Insarov (Jun 17 2021 at 15:08):It works, thanks! Why does one work but not the other?
Pierre-Marie Pédrot (Jun 17 2021 at 15:16):https://coq.inria.fr/doc/language/core/inductive.html#the-match-with-end-construction
Pierre-Marie Pédrot (Jun 17 2021 at 15:16):in particular the paragraph about Prop
Last updated: Sep 23 2023 at 15:01 UTC